Theorem cflim 4909

Description: Value of the cofinality function at a limit ordinal. Part of Definition of cofinality of [Enderton] p. 257.

Assertion

Ref	Expression
cflim	|- ((A e. B /\ Lim A) -> (cf` A) = |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))})

Distinct variable group:   x,y,A

Proof of Theorem cflim

Step	Hyp	Ref	Expression
1		limsuc 3120	. . . . . . . . . . . . . . . . . . . 20 |- (Lim A -> (v e. A <-> suc v e. A))
2	1	biimpd 153	. . . . . . . . . . . . . . . . . . 19 |- (Lim A -> (v e. A -> suc v e. A))
3		sseq1 2082	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = suc v -> (z (_ w <-> suc v (_ w))
4	3	rexbidv 1664	. . . . . . . . . . . . . . . . . . . . 21 |- (z = suc v -> (E.w e. y z (_ w <-> E.w e. y suc v (_ w))
5	4	rcla4v 1873	. . . . . . . . . . . . . . . . . . . 20 |- (suc v e. A -> (A.z e. A E.w e. y z (_ w -> E.w e. y suc v (_ w))
6		visset 1813	. . . . . . . . . . . . . . . . . . . . . . 23 |- v e. V
7		sucssel 3070	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. V -> (suc v (_ w -> v e. w))
8	6, 7	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . 22 |- (suc v (_ w -> v e. w)
9	8	r19.22si 1734	. . . . . . . . . . . . . . . . . . . . 21 |- (E.w e. y suc v (_ w -> E.w e. y v e. w)
10		eluni2 2507	. . . . . . . . . . . . . . . . . . . . 21 |- (v e. U.y <-> E.w e. y v e. w)
11	9, 10	sylibr 200	. . . . . . . . . . . . . . . . . . . 20 |- (E.w e. y suc v (_ w -> v e. U.y)
12	5, 11	syl6com 53	. . . . . . . . . . . . . . . . . . 19 |- (A.z e. A E.w e. y z (_ w -> (suc v e. A -> v e. U.y))
13	2, 12	syl9 57	. . . . . . . . . . . . . . . . . 18 |- (Lim A -> (A.z e. A E.w e. y z (_ w -> (v e. A -> v e. U.y)))
14	13	r19.21adv 1718	. . . . . . . . . . . . . . . . 17 |- (Lim A -> (A.z e. A E.w e. y z (_ w -> A.v e. A v e. U.y))
15		dfss3 2059	. . . . . . . . . . . . . . . . 17 |- (A (_ U.y <-> A.v e. A v e. U.y)
16	14, 15	syl6ibr 213	. . . . . . . . . . . . . . . 16 |- (Lim A -> (A.z e. A E.w e. y z (_ w -> A (_ U.y))
17	16	adantr 389	. . . . . . . . . . . . . . 15 |- ((Lim A /\ y (_ A) -> (A.z e. A E.w e. y z (_ w -> A (_ U.y))
18		limuni 3029	. . . . . . . . . . . . . . . . . 18 |- (Lim A -> A = U.A)
19	18	sseq2d 2089	. . . . . . . . . . . . . . . . 17 |- (Lim A -> (U.y (_ A <-> U.y (_ U.A))
20		uniss 2521	. . . . . . . . . . . . . . . . 17 |- (y (_ A -> U.y (_ U.A)
21	19, 20	syl5bir 210	. . . . . . . . . . . . . . . 16 |- (Lim A -> (y (_ A -> U.y (_ A))
22	21	imp 350	. . . . . . . . . . . . . . 15 |- ((Lim A /\ y (_ A) -> U.y (_ A)
23	17, 22	jctird 602	. . . . . . . . . . . . . 14 |- ((Lim A /\ y (_ A) -> (A.z e. A E.w e. y z (_ w -> (A (_ U.y /\ U.y (_ A)))
24		eqss 2077	. . . . . . . . . . . . . 14 |- (A = U.y <-> (A (_ U.y /\ U.y (_ A))
25	23, 24	syl6ibr 213	. . . . . . . . . . . . 13 |- ((Lim A /\ y (_ A) -> (A.z e. A E.w e. y z (_ w -> A = U.y))
26	25	ex 373	. . . . . . . . . . . 12 |- (Lim A -> (y (_ A -> (A.z e. A E.w e. y z (_ w -> A = U.y)))
27	26	imdistand 445	. . . . . . . . . . 11 |- (Lim A -> ((y (_ A /\ A.z e. A E.w e. y z (_ w) -> (y (_ A /\ A = U.y)))
28	27	anim2d 561	. . . . . . . . . 10 |- (Lim A -> ((x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w)) -> (x = (card` y) /\ (y (_ A /\ A = U.y))))
29	28	19.22dv 1290	. . . . . . . . 9 |- (Lim A -> (E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w)) -> E.y(x = (card` y) /\ (y (_ A /\ A = U.y))))
30	29	19.21aiv 1286	. . . . . . . 8 |- (Lim A -> A.x(E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w)) -> E.y(x = (card` y) /\ (y (_ A /\ A = U.y))))
31		ss2ab 2116	. . . . . . . 8 |- ({x | E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w))} (_ {x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} <-> A.x(E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w)) -> E.y(x = (card` y) /\ (y (_ A /\ A = U.y))))
32	30, 31	sylibr 200	. . . . . . 7 |- (Lim A -> {x | E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w))} (_ {x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))})
33		intss 2554	. . . . . . 7 |- ({x | E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w))} (_ {x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} -> |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w))})
34	32, 33	syl 10	. . . . . 6 |- (Lim A -> |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w))})
35	34	adantl 388	. . . . 5 |- ((A e. V /\ Lim A) -> |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w))})
36		limelon 3032	. . . . . 6 |- ((A e. V /\ Lim A) -> A e. On)
37		cfval 4906	. . . . . 6 |- (A e. On -> (cf` A) = |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w))})
38	36, 37	syl 10	. . . . 5 |- ((A e. V /\ Lim A) -> (cf` A) = |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w))})
39	35, 38	sseqtr4d 2098	. . . 4 |- ((A e. V /\ Lim A) -> |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} (_ (cf` A))
40		cfub 4908	. . . . 5 |- (cf` A) (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A (_ U.y))}
41		eqimss 2109	. . . . . . . . . 10 |- (A = U.y -> A (_ U.y)
42	41	anim2i 335	. . . . . . . . 9 |- ((y (_ A /\ A = U.y) -> (y (_ A /\ A (_ U.y))
43	42	anim2i 335	. . . . . . . 8 |- ((x = (card` y) /\ (y (_ A /\ A = U.y)) -> (x = (card` y) /\ (y (_ A /\ A (_ U.y)))
44	43	19.22i 1040	. . . . . . 7 |- (E.y(x = (card` y) /\ (y (_ A /\ A = U.y)) -> E.y(x = (card` y) /\ (y (_ A /\ A (_ U.y)))
45	44	ss2abi 2120	. . . . . 6 |- {x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} (_ {x | E.y(x = (card` y) /\ (y (_ A /\ A (_ U.y))}
46		intss 2554	. . . . . 6 |- ({x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} (_ {x | E.y(x = (card` y) /\ (y (_ A /\ A (_ U.y))} -> |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A (_ U.y))} (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))})
47	45, 46	ax-mp 7	. . . . 5 |- |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A (_ U.y))} (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))}
48	40, 47	sstri 2073	. . . 4 |- (cf` A) (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))}
49	39, 48	jctil 292	. . 3 |- ((A e. V /\ Lim A) -> ((cf` A) (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} /\ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} (_ (cf` A)))
50		eqss 2077	. . 3 |- ((cf` A) = |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} <-> ((cf` A) (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} /\ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} (_ (cf` A)))
51	49, 50	sylibr 200	. 2