Theorem cfsuc 4895

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 3063	. . 3 |- (A e. On <-> suc A e. On)
2		cfval 4886	. . 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 199	. 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 2745	. . . . . . 7 |- {A} e. V
5		fveq2 3715	. . . . . . . . 9 |- (y = {A} -> (card` y) = (card` {A}))
6	5	eqeq2d 1483	. . . . . . . 8 |- (y = {A} -> (1o = (card` y) <-> 1o = (card` {A})))
7		sseq1 2078	. . . . . . . . 9 |- (y = {A} -> (y (_ suc A <-> {A} (_ suc A))
8		rexeq1 1784	. . . . . . . . . 10 |- (y = {A} -> (E.w e. y z (_ w <-> E.w e. {A}z (_ w))
9	8	ralbidv 1660	. . . . . . . . 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 627	. . . . . . . 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 627	. . . . . . 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 1865	. . . . . 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 4814	. . . . . . 7 |- (A e. On -> (card` {A}) = 1o)
14	13	eqcomd 1477	. . . . . 6 |- (A e. On -> 1o = (card` {A}))
15		onelsst 2995	. . . . . . . . . . . 12 |- (A e. On -> (z e. A -> z (_ A))
16		eqimss 2105	. . . . . . . . . . . . 13 |- (z = A -> z (_ A)
17	16	a1i 8	. . . . . . . . . . . 12 |- (A e. On -> (z = A -> z (_ A))
18	15, 17	jaod 424	. . . . . . . . . . 11 |- (A e. On -> ((z e. A \/ z = A) -> z (_ A))
19		elsuci 3030	. . . . . . . . . . 11 |- (z e. suc A -> (z e. A \/ z = A))
20	18, 19	syl5 21	. . . . . . . . . 10 |- (A e. On -> (z e. suc A -> z (_ A))
21		snidg 2429	. . . . . . . . . 10 |- (A e. On -> A e. {A})
22	20, 21	jctild 600	. . . . . . . . 9 |- (A e. On -> (z e. suc A -> (A e. {A} /\ z (_ A)))
23		sseq2 2079	. . . . . . . . . 10 |- (w = A -> (z (_ w <-> z (_ A))
24	23	rcla4ev 1873	. . . . . . . . 9 |- ((A e. {A} /\ z (_ A) -> E.w e. {A}z (_ w)
25	22, 24	syl6 22	. . . . . . . 8 |- (A e. On -> (z e. suc A -> E.w e. {A}z (_ w))
26	25	r19.21aiv 1710	. . . . . . 7 |- (A e. On -> A.z e. suc AE.w e. {A}z (_ w)
27		ssun2 2190	. . . . . . . 8 |- {A} (_ (A u. {A})
28		df-suc 2949	. . . . . . . 8 |- suc A = (A u. {A})
29	27, 28	sseqtr4 2090	. . . . . . 7 |- {A} (_ suc A
30	26, 29	jctil 292	. . . . . 6 |- (A e. On -> ({A} (_ suc A /\ A.z e. suc AE.w e. {A}z (_ w))
31	12, 14, 30	sylanc 471	. . . . 5 |- (A e. On -> E.y(1o = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w)))
32		1on 4128	. . . . . . 7 |- 1o e. On
33	32	elisseti 1814	. . . . . 6 |- 1o e. V
34		eqeq1 1478	. . . . . . . 8 |- (x = 1o -> (x = (card` y) <-> 1o = (card` y)))
35	34	anbi1d 616	. . . . . . 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))))
36	35	exbidv 1277	. . . . . 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))))
37	33, 36	elab 1893	. . . . 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)))
38	31, 37	sylibr 200	. . . 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))})
39		el1o 4136	. . . . . 6 |- (v e. 1o <-> v = (/))
40		eqcom 1474	. . . . . . . . . . . . 13 |- ((/) = (card` y) <-> (card` y) = (/))
41		visset 1809	. . . . . . . . . . . . . 14 |- y e. V
42		cardeq0 4812	. . . . . . . . . . . . . 14 |- (y e. V -> ((card` y) = (/) <-> y = (/)))
43	41, 42	ax-mp 7	. . . . . . . . . . . . 13 |- ((card` y) = (/) <-> y = (/))
44	40, 43	bitr 173	. . . . . . . . . . . 12 |- ((/) = (card` y) <-> y = (/))
45		rex0 2287	. . . . . . . . . . . . . . . 16 |- -. E.w e. (/) z (_ w
46	45	a1i 8	. . . . . . . . . . . . . . 15 |- (z e. suc A -> -. E.w e. (/) z (_ w)
47	46	nrex 1726	. . . . . . . . . . . . . 14 |- -. E.z e. suc AE.w e. (/) z (_ w
48		nsuceq0 3048	. . . . . . . . . . . . . . 15 |- suc A =/= (/)
49		r19.2z 2343	. . . . . . . . . . . . . . 15 |- ((suc A =/= (/) /\ A.z e. suc AE.w e. (/) z (_ w) -> E.z e. suc AE.w e. (/) z (_ w)
50	48, 49	mpan 694	. . . . . . . . . . . . . 14 |- (A.z e. suc AE.w e. (/) z (_ w -> E.z e. suc AE.w e. (/) z (_ w)
51	47, 50	mto 106	. . . . . . . . . . . . 13 |- -. A.z e. suc AE.w e. (/) z (_ w
52		rexeq1 1784	. . . . . . . . . . . . . 14 |- (y = (/) -> (E.w e. y z (_ w <-> E.w e. (/) z (_ w))
53	52	ralbidv 1660	. . . . . . . . . . . . 13 |- (y = (/) -> (A.z e. suc AE.w e. y z (_ w <-> A.z e. suc AE.w e. (/) z (_ w))
54	51, 53	mtbiri 716	. . . . . . . . . . . 12 |- (y = (/) -> -. A.z e. suc AE.w e. y z (_ w)
55	44, 54	sylbi 199	. . . . . . . . . . 11 |- ((/) = (card` y) -> -. A.z e. suc AE.w e. y z (_ w)
56	55	intnand 692	. . . . . . . . . 10 |- ((/) = (card` y) -> -. (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))
57		imnan 242	. . . . . . . . . 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)))
58	56, 57	mpbi 189	. . . . . . . . 9 |- -. ((/) = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))
59	58	nex 1099	. . . . . . . 8 |- -. E.y((/) = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))
60		0ex 2706	. . . . . . . . 9 |- (/) e. V
61		eqeq1 1478	. . . . . . . . . . 11 |- (x = (/) -> (x = (card` y) <-> (/) = (card` y)))
62	61	anbi1d 616	. . . . . . . . . 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))))
63	62	exbidv 1277	. . . . . . . . 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))))
64	60, 63	elab 1893	. . . . . . . 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)))
65	59, 64	mtbir 192	. . . . . . 7 |- -. (/) e. {x | E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))}
66		eleq1 1531	. . . . . . 7 |- (v = (/) -> (v e. {x | E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))} <-> (/) e. {x | E.y(x = (card` y) /\ (y (_ suc A /\ A.z e. suc AE.w e. y z (_ w))}))
67	65, 66	mtbiri 716	. . . . . 6 |-