Theorem cfsuc 3709

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

Assertion

Ref	Expression
cfsuc	|- (A e. On -> (cf` suc A) = 1o)

Proof of Theorem cfsuc

Step	Hyp	Ref	Expression
1		sucelon 2319	. . 3 |- (A e. On <-> suc A e. On)
2		cfval 3701	. . 3 |- (suc A e. On -> (cf` suc A) = |^|{x | E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))})
3	1, 2	sylbi 174	. 2 |- (A e. On -> (cf` suc A) = |^|{x | E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))})
4		snex 1859	. . . . . . 7 |- {A} e. 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} -> (E.w e. y z (_ w <-> E.w e. {A}z (_ w))
9	8	biraldv 1219	. . . . . . . . 9 |- (y = {A} -> (A.z e. suc AE.w e. y z (_ w <-> A.z e. suc AE.w e. {A}z (_ w))
10	7, 9	anbi12d 476	. . . . . . . 8 |- (y = {A} -> ((y (_ suc A /\ A.z e. suc AE.w e. y z (_ w) <-> ({A} (_ suc A /\ A.z e. suc AE.w e. {A}z (_ w)))
11	6, 10	anbi12d 476	. . . . . . 7 |- (y = {A} -> ((1o = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)) <-> (1o = (card` {A}) /\ ({A} (_ suc A /\ A.z e. suc AE.w e. {A}z (_ w))))
12	4, 11	cla4ev 1401	. . . . . 6 |- ((1o = (card` {A}) /\ ({A} (_ suc A /\ A.z e. suc AE.w e. {A}z (_ w)) -> E.y(1o = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)))
13		cardsn 3640	. . . . . . 7 |- (A e. On -> (card` {A}) = 1o)
14	13	cleqcomd 1106	. . . . . 6 |- (A e. On -> 1o = (card` {A}))
15		snidg 1828	. . . . . . . . . . 11 |- (A e. On -> A e. {A})
16	15	a1d 14	. . . . . . . . . 10 |- (A e. On -> (z e. suc A -> A e. {A}))
17		onelsst 2255	. . . . . . . . . . . 12 |- (A e. On -> (z e. A -> z (_ A))
18		eqimss 1548	. . . . . . . . . . . . 13 |- (z = A -> z (_ A)
19	18	a1i 7	. . . . . . . . . . . 12 |- (A e. On -> (z = A -> z (_ A))
20	17, 19	jaod 329	. . . . . . . . . . 11 |- (A e. On -> ((z e. A \/ z = A) -> z (_ A))
21		elsuci 2289	. . . . . . . . . . 11 |- (z e. suc A -> (z e. A \/ z = A))
22	20, 21	syl5 22	. . . . . . . . . 10 |- (A e. On -> (z e. suc A -> z (_ A))
23	16, 22	jcad 455	. . . . . . . . 9 |- (A e. On -> (z e. suc A -> (A e. {A} /\ z (_ A)))
24		sseq2 1522	. . . . . . . . . 10 |- (w = A -> (z (_ w <-> z (_ A))
25	24	rcla4ev 1403	. . . . . . . . 9 |- ((A e. {A} /\ z (_ A) -> E.w e. {A}z (_ w)
26	23, 25	syl6 23	. . . . . . . 8 |- (A e. On -> (z e. suc A -> E.w e. {A}z (_ w))
27	26	r19.21aiv 1259	. . . . . . 7 |- (A e. On -> A.z e. suc AE.w e. {A}z (_ w)
28		ssun2 1622	. . . . . . . 8 |- {A} (_ (A u. {A})
29		df-suc 2205	. . . . . . . 8 |- suc A = (A u. {A})
30	28, 29	sseqtr4 1533	. . . . . . 7 |- {A} (_ suc A
31	27, 30	jctil 240	. . . . . 6 |- (A e. On -> ({A} (_ suc A /\ A.z e. suc AE.w e. {A}z (_ w))
32	12, 14, 31	sylanc 361	. . . . 5 |- (A e. On -> E.y(1o = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)))
33		1o 3109	. . . . . . 7 |- 1o e. On
34	33	elisseti 1355	. . . . . 6 |- 1o e. 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 /\ A.z e. suc AE.w e. y z (_ w)) <-> (1o = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))))
37	36	biexdv 936	. . . . . 6 |- (x = 1o -> (E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)) <-> E.y(1o = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))))
38	34, 37	elab 1415	. . . . 5 |- (1o e. {x | E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))} <-> E.y(1o = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)))
39	32, 38	sylibr 175	. . . 4 |- (A e. On -> 1o e. {x | E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))})
40		df1o2 3111	. . . . . . . 8 |- 1o = {(/)}
41	40	eleq2i 1153	. . . . . . 7 |- (v e. 1o <-> v e. {(/)})
42		elsn 1820	. . . . . . 7 |- (v e. {(/)} <-> v = (/))
43	41, 42	bitr 151	. . . . . 6 |- (v e. 1o <-> v = (/))
44		cleqcom 1103	. . . . . . . . . . . . . 14 |- ((/) = (card` y) <-> (card` y) = (/))
45		visset 1350	. . . . . . . . . . . . . . 15 |- y e. V
46		cardeq0 3639	. . . . . . . . . . . . . . 15 |- (y e. 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 |- -. E.w e. (/) z (_ w
50	49	a1i 7	. . . . . . . . . . . . . . . 16 |- (z e. suc A -> -. E.w e. (/) z (_ w)
51	50	nrex 1270	. . . . . . . . . . . . . . 15 |- -. E.z e. suc AE.w e. (/) z (_ w
52		nsuceq0 2306	. . . . . . . . . . . . . . . 16 |- -. suc A = (/)
53		r19.2z 1766	. . . . . . . . . . . . . . . 16 |- (-. suc A = (/) -> (A.z e. suc AE.w e. (/) z (_ w -> E.z e. suc AE.w e. (/) z (_ w))
54	52, 53	ax-mp 6	. . . . . . . . . . . . . . 15 |- (A.z e. suc AE.w e. (/) z (_ w -> E.z e. suc AE.w e. (/) z (_ w)
55	51, 54	mto 93	. . . . . . . . . . . . . 14 |- -. A.z e. suc AE.w e. (/) z (_ w
56		rexeq 1325	. . . . . . . . . . . . . . 15 |- (y = (/) -> (E.w e. y z (_ w <-> E.w e. (/) z (_ w))
57	56	biraldv 1219	. . . . . . . . . . . . . 14 |- (y = (/) -> (A.z e. suc AE.w e. y z (_ w <-> A.z e. suc AE.w e. (/) z (_ w))
58	55, 57	mtbiri 539	. . . . . . . . . . . . 13 |- (y = (/) -> -. A.z e. suc AE.w e. y z (_ w)
59	48, 58	sylbi 174	. . . . . . . . . . . 12 |- ((/) = (card` y) -> -. A.z e. suc AE.w e. y z (_ w)
60	59	adantr 306	. . . . . . . . . . 11 |- (((/) = (card` y) /\ y (_ suc A) -> -. A.z e. suc AE.w e. y z (_ w)
61		nan 514	. . . . . . . . . . 11 |- (((/) = (card` y) -> -. (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)) <-> (((/) = (card` y) /\ y (_ suc A) -> -. A.z e. suc AE.w e. y z (_ w))
62	60, 61	mpbir 165	. . . . . . . . . 10 |- ((/) = (card` y) -> -. (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))
63		imnan 207	. . . . . . . . . 10 |- (((/) = (card` y) -> -. (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)) <-> -. ((/) = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)))
64	62, 63	mpbi 164	. . . . . . . . 9 |- -. ((/) = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))
65	64	nex 779	. . . . . . . 8 |- -. E.y((/) = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))
66		0ex 1745	. . . . . . . . 9 |- (/) e. V
67		cleq1 1107	. . . . . . . . . . 11 |- (x = (/) -> (x = (card` y) <-> (/) = (card` y)))
68	67	anbi1d 469	. . . . . . . . . 10 |- (x = (/) -> ((x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)) <-> ((/) = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))))
69	68	biexdv 936	. . . . . . . . 9 |- (x = (/) -> (E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)) <-> E.y((/) = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))))
70	66, 69	elab 1415	. . . . . . . 8 |- ((/) e. {x | E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))} <-> E.y((/) = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)))
71	65, 70	mtbir 167	. . . . . . 7 |- -. (/) e. {x | E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))}
72		eleq1 1149	. . . . . . 7 |- (v