Theorem cfsuc 3709

Description: Value of the cofinality function at a successor ordinal. Exercise 3 of [TakeutiZaring] p. 102.

Assertion

Ref	Expression
cfsuc	⊢ (A ∈ On → (cf ‘suc A) = 1o)

Proof of Theorem cfsuc

Step	Hyp	Ref	Expression
1		sucelon 2319	. . 3 ⊢ (A ∈ On ↔ suc A ∈ On)
2		cfval 3701	. . 3 ⊢ (suc A ∈ On → (cf ‘suc A) = ∩{x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))})
3	1, 2	sylbi 174	. 2 ⊢ (A ∈ On → (cf ‘suc A) = ∩{x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))})
4		snex 1859	. . . . . . 7 ⊢ {A} ∈ V
5		fveq2 2832	. . . . . . . . 9 ⊢ (y = {A} → (card ‘y) = (card ‘{A}))
6	5	cleq2d 1112	. . . . . . . 8 ⊢ (y = {A} → (1o = (card ‘y) ↔ 1o = (card ‘{A})))
7		sseq1 1521	. . . . . . . . 9 ⊢ (y = {A} → (y ⊆ suc A ↔ {A} ⊆ suc A))
8		rexeq 1325	. . . . . . . . . 10 ⊢ (y = {A} → (∃w ∈ y z ⊆ w ↔ ∃w ∈ {A}z ⊆ w))
9	8	biraldv 1219	. . . . . . . . 9 ⊢ (y = {A} → (∀z ∈ suc A∃w ∈ y z ⊆ w ↔ ∀z ∈ suc A∃w ∈ {A}z ⊆ w))
10	7, 9	anbi12d 476	. . . . . . . 8 ⊢ (y = {A} → ((y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w) ↔ ({A} ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ {A}z ⊆ w)))
11	6, 10	anbi12d 476	. . . . . . 7 ⊢ (y = {A} → ((1o = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)) ↔ (1o = (card ‘{A}) ∧ ({A} ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ {A}z ⊆ w))))
12	4, 11	cla4ev 1401	. . . . . 6 ⊢ ((1o = (card ‘{A}) ∧ ({A} ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ {A}z ⊆ w)) → ∃y(1o = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)))
13		cardsn 3640	. . . . . . 7 ⊢ (A ∈ On → (card ‘{A}) = 1o)
14	13	cleqcomd 1106	. . . . . 6 ⊢ (A ∈ On → 1o = (card ‘{A}))
15		snidg 1828	. . . . . . . . . . 11 ⊢ (A ∈ On → A ∈ {A})
16	15	a1d 14	. . . . . . . . . 10 ⊢ (A ∈ On → (z ∈ suc A → A ∈ {A}))
17		onelsst 2255	. . . . . . . . . . . 12 ⊢ (A ∈ On → (z ∈ A → z ⊆ A))
18		eqimss 1548	. . . . . . . . . . . . 13 ⊢ (z = A → z ⊆ A)
19	18	a1i 7	. . . . . . . . . . . 12 ⊢ (A ∈ On → (z = A → z ⊆ A))
20	17, 19	jaod 329	. . . . . . . . . . 11 ⊢ (A ∈ On → ((z ∈ A ∨ z = A) → z ⊆ A))
21		elsuci 2289	. . . . . . . . . . 11 ⊢ (z ∈ suc A → (z ∈ A ∨ z = A))
22	20, 21	syl5 22	. . . . . . . . . 10 ⊢ (A ∈ On → (z ∈ suc A → z ⊆ A))
23	16, 22	jcad 455	. . . . . . . . 9 ⊢ (A ∈ On → (z ∈ suc A → (A ∈ {A} ∧ z ⊆ A)))
24		sseq2 1522	. . . . . . . . . 10 ⊢ (w = A → (z ⊆ w ↔ z ⊆ A))
25	24	rcla4ev 1403	. . . . . . . . 9 ⊢ ((A ∈ {A} ∧ z ⊆ A) → ∃w ∈ {A}z ⊆ w)
26	23, 25	syl6 23	. . . . . . . 8 ⊢ (A ∈ On → (z ∈ suc A → ∃w ∈ {A}z ⊆ w))
27	26	r19.21aiv 1259	. . . . . . 7 ⊢ (A ∈ On → ∀z ∈ suc A∃w ∈ {A}z ⊆ w)
28		ssun2 1622	. . . . . . . 8 ⊢ {A} ⊆ (A ∪ {A})
29		df-suc 2205	. . . . . . . 8 ⊢ suc A = (A ∪ {A})
30	28, 29	sseqtr4 1533	. . . . . . 7 ⊢ {A} ⊆ suc A
31	27, 30	jctil 240	. . . . . 6 ⊢ (A ∈ On → ({A} ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ {A}z ⊆ w))
32	12, 14, 31	sylanc 361	. . . . 5 ⊢ (A ∈ On → ∃y(1o = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)))
33		1o 3109	. . . . . . 7 ⊢ 1o ∈ On
34	33	elisseti 1355	. . . . . 6 ⊢ 1o ∈ V
35		cleq1 1107	. . . . . . . 8 ⊢ (x = 1o → (x = (card ‘y) ↔ 1o = (card ‘y)))
36	35	anbi1d 469	. . . . . . 7 ⊢ (x = 1o → ((x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)) ↔ (1o = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))))
37	36	biexdv 936	. . . . . 6 ⊢ (x = 1o → (∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)) ↔ ∃y(1o = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))))
38	34, 37	elab 1415	. . . . 5 ⊢ (1o ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))} ↔ ∃y(1o = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)))
39	32, 38	sylibr 175	. . . 4 ⊢ (A ∈ On → 1o ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))})
40		df1o2 3111	. . . . . . . 8 ⊢ 1o = {∅}
41	40	eleq2i 1153	. . . . . . 7 ⊢ (v ∈ 1o ↔ v ∈ {∅})
42		elsn 1820	. . . . . . 7 ⊢ (v ∈ {∅} ↔ v = ∅)
43	41, 42	bitr 151	. . . . . 6 ⊢ (v ∈ 1o ↔ v = ∅)
44		cleqcom 1103	. . . . . . . . . . . . . 14 ⊢ (∅ = (card ‘y) ↔ (card ‘y) = ∅)
45		visset 1350	. . . . . . . . . . . . . . 15 ⊢ y ∈ V
46		cardeq0 3639	. . . . . . . . . . . . . . 15 ⊢ (y ∈ V → ((card ‘y) = ∅ ↔ y = ∅))
47	45, 46	ax-mp 6	. . . . . . . . . . . . . 14 ⊢ ((card ‘y) = ∅ ↔ y = ∅)
48	44, 47	bitr 151	. . . . . . . . . . . . 13 ⊢ (∅ = (card ‘y) ↔ y = ∅)
49		rex0 1717	. . . . . . . . . . . . . . . . 17 ⊢ ¬ ∃w ∈ ∅ z ⊆ w
50	49	a1i 7	. . . . . . . . . . . . . . . 16 ⊢ (z ∈ suc A → ¬ ∃w ∈ ∅ z ⊆ w)
51	50	nrex 1270	. . . . . . . . . . . . . . 15 ⊢ ¬ ∃z ∈ suc A∃w ∈ ∅ z ⊆ w
52		nsuceq0 2306	. . . . . . . . . . . . . . . 16 ⊢ ¬ suc A = ∅
53		r19.2z 1766	. . . . . . . . . . . . . . . 16 ⊢ (¬ suc A = ∅ → (∀z ∈ suc A∃w ∈ ∅ z ⊆ w → ∃z ∈ suc A∃w ∈ ∅ z ⊆ w))
54	52, 53	ax-mp 6	. . . . . . . . . . . . . . 15 ⊢ (∀z ∈ suc A∃w ∈ ∅ z ⊆ w → ∃z ∈ suc A∃w ∈ ∅ z ⊆ w)
55	51, 54	mto 93	. . . . . . . . . . . . . 14 ⊢ ¬ ∀z ∈ suc A∃w ∈ ∅ z ⊆ w
56		rexeq 1325	. . . . . . . . . . . . . . 15 ⊢ (y = ∅ → (∃w ∈ y z ⊆ w ↔ ∃w ∈ ∅ z ⊆ w))
57	56	biraldv 1219	. . . . . . . . . . . . . 14 ⊢ (y = ∅ → (∀z ∈ suc A∃w ∈ y z ⊆ w ↔ ∀z ∈ suc A∃w ∈ ∅ z ⊆ w))
58	55, 57	mtbiri 539	. . . . . . . . . . . . 13 ⊢ (y = ∅ → ¬ ∀z ∈ suc A∃w ∈ y z ⊆ w)
59	48, 58	sylbi 174	. . . . . . . . . . . 12 ⊢ (∅ = (card ‘y) → ¬ ∀z ∈ suc A∃w ∈ y z ⊆ w)
60	59	adantr 306	. . . . . . . . . . 11 ⊢ ((∅ = (card ‘y) ∧ y ⊆ suc A) → ¬ ∀z ∈ suc A∃w ∈ y z ⊆ w)
61		nan 514	. . . . . . . . . . 11 ⊢ ((∅ = (card ‘y) → ¬ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)) ↔ ((∅ = (card ‘y) ∧ y ⊆ suc A) → ¬ ∀z ∈ suc A∃w ∈ y z ⊆ w))
62	60, 61	mpbir 165	. . . . . . . . . 10 ⊢ (∅ = (card ‘y) → ¬ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))
63		imnan 207	. . . . . . . . . 10 ⊢ ((∅ = (card ‘y) → ¬ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)) ↔ ¬ (∅ = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)))
64	62, 63	mpbi 164	. . . . . . . . 9 ⊢ ¬ (∅ = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))
65	64	nex 779	. . . . . . . 8 ⊢ ¬ ∃y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))
66		0ex 1745	. . . . . . . . 9 ⊢ ∅ ∈ V
67		cleq1 1107	. . . . . . . . . . 11 ⊢ (x = ∅ → (x = (card ‘y) ↔ ∅ = (card ‘y)))
68	67	anbi1d 469	. . . . . . . . . 10 ⊢ (x = ∅ → ((x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)) ↔ (∅ = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))))
69	68	biexdv 936	. . . . . . . . 9 ⊢ (x = ∅ → (∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)) ↔ ∃y(∅ = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))))
70	66, 69	elab 1415	. . . . . . . 8 ⊢ (∅ ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))} ↔ ∃y(∅ = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)))
71	65, 70	mtbir 167	. . . . . . 7 ⊢ ¬ ∅ ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))}
72		eleq1 1149	. . . . . . 7 ⊢ (v = ∅ → (v ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))} ↔ ∅ ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))}))
73	71, 72	mtbiri 539	. . . . . 6 ⊢ (v = ∅ → ¬ v ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))})
74	43, 73	sylbi 174	. . . . 5 ⊢ (v ∈ 1o → ¬ v ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))})
75	74	rgen 1247	. . . 4 ⊢ ∀v ∈ 1o ¬ v ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))}
76	39, 75	jctir 241	. . 3 ⊢ (A ∈ On → (1o ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))} ∧ ∀v ∈ 1o ¬ v ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))}))
77		cardon 3634	. . . . . . . . 9 ⊢ (card ‘y) ∈ On
78		eleq1 1149	. . . . . . . . 9 ⊢ (x = (card ‘y) → (x ∈ On ↔ (card ‘y) ∈ On))
79	77, 78	mpbiri 169	. . . . . . . 8 ⊢ (x = (card ‘y) → x ∈ On)
80	79	adantr 306	. . . . . . 7 ⊢ ((x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)) → x ∈ On)
81	80	19.23aiv 952	. . . . . 6 ⊢ (∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w)) → x ∈ On)
82	81	ss2abi 1552	. . . . 5 ⊢ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))} ⊆ {x∣x ∈ On}
83		abid2 1186	. . . . 5 ⊢ {x∣x ∈ On} = On
84	82, 83	sseqtr 1532	. . . 4 ⊢ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))} ⊆ On
85		oneqmini 2272	. . . 4 ⊢ ({x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))} ⊆ On → ((1o ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))} ∧ ∀v ∈ 1o ¬ v ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))}) → 1o = ∩{x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))}))
86	84, 85	ax-mp 6	. . 3 ⊢ ((1o ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))} ∧ ∀v ∈ 1o ¬ v ∈ {x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))}) → 1o = ∩{x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))})
87	76, 86	syl 12	. 2 ⊢ (A ∈ On → 1o = ∩{x∣∃y(x = (card ‘y) ∧ (y ⊆ suc A ∧ ∀z ∈ suc A∃w ∈ y z ⊆ w))})
88	3, 87	eqtr4d 1131	1 ⊢ (A ∈ On → (cf ‘suc A) = 1o)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196  ∃wex 678  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  Vcvv 1348   ∪ cun 1485   ⊆ wss 1487  ∅c0 1707  {csn 1808  ∩cint 1965  Oncon0 2199  suc csuc 2201   ‘cfv 2422  1_oc1o 3099  cardccrd 3620  cfccf 3622

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-ac 1080

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif <-PAN CLASS=r STYLE="color:#82A800">1489  df-un 1490  df-in 1491  df•ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-1o 3104  df-er 3200  df-en 3274  df-dom 3275  df-sdom 3276  df-car 3623  df-cf 3625

metamath.org