Theorem cflim 3704

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(s):   x,y,A

Proof of Theorem cflim

Step	Hyp	Ref	Expression
1		limsuc 2361	. . . . . . . . . . . . . . . . . . . 20 |- (Lim A -> (v e. A <-> suc v e. A))
2	1	biimpd 135	. . . . . . . . . . . . . . . . . . 19 |- (Lim A -> (v e. A -> suc v e. A))
3		sseq1 1521	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = suc v -> (z (_ w <-> suc v (_ w))
4	3	birexdv 1220	. . . . . . . . . . . . . . . . . . . . 21 |- (z = suc v -> (E.w e. y z (_ w <-> E.w e. y suc v (_ w))
5	4	rcla4v 1402	. . . . . . . . . . . . . . . . . . . 20 |- (A.z e. A E.w e. y z (_ w -> (suc v e. A -> E.w e. y suc v (_ w))
6		visset 1350	. . . . . . . . . . . . . . . . . . . . . . 23 |- v e. V
7		sucssel 2321	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. V -> (suc v (_ w -> v e. w))
8	6, 7	ax-mp 6	. . . . . . . . . . . . . . . . . . . . . 22 |- (suc v (_ w -> v e. w)
9	8	r19.22si 1275	. . . . . . . . . . . . . . . . . . . . 21 |- (E.w e. y suc v (_ w -> E.w e. y v e. w)
10		eluni2 1923	. . . . . . . . . . . . . . . . . . . . 21 |- (v e. U.y <-> E.w e. y v e. w)
11	9, 10	sylibr 175	. . . . . . . . . . . . . . . . . . . 20 |- (E.w e. y suc v (_ w -> v e. U.y)
12	5, 11	syl6 23	. . . . . . . . . . . . . . . . . . 19 |- (A.z e. A E.w e. y z (_ w -> (suc v e. A -> v e. U.y))
13	2, 12	syl9 55	. . . . . . . . . . . . . . . . . 18 |- (Lim A -> (A.z e. A E.w e. y z (_ w -> (v e. A -> v e. U.y)))
14	13	r19.21adv 1262	. . . . . . . . . . . . . . . . 17 |- (Lim A -> (A.z e. A E.w e. y z (_ w -> A.v e. A v e. U.y))
15		dfss3 1498	. . . . . . . . . . . . . . . . 17 |- (A (_ U.y <-> A.v e. A v e. U.y)
16	14, 15	syl6ibr 186	. . . . . . . . . . . . . . . 16 |- (Lim A -> (A.z e. A E.w e. y z (_ w -> A (_ U.y))
17	16	adantr 306	. . . . . . . . . . . . . . 15 |- ((Lim A /\ y (_ A) -> (A.z e. A E.w e. y z (_ w -> A (_ U.y))
18		limuni 2284	. . . . . . . . . . . . . . . . . . 19 |- (Lim A -> A = U.A)
19	18	sseq2d 1528	. . . . . . . . . . . . . . . . . 18 |- (Lim A -> (U.y (_ A <-> U.y (_ U.A))
20		uniss 1936	. . . . . . . . . . . . . . . . . 18 |- (y (_ A -> U.y (_ U.A)
21	19, 20	syl5bir 184	. . . . . . . . . . . . . . . . 17 |- (Lim A -> (y (_ A -> U.y (_ A))
22	21	imp 277	. . . . . . . . . . . . . . . 16 |- ((Lim A /\ y (_ A) -> U.y (_ A)
23	22	a1d 14	. . . . . . . . . . . . . . 15 |- ((Lim A /\ y (_ A) -> (A.z e. A E.w e. y z (_ w -> U.y (_ A))
24	17, 23	jcad 455	. . . . . . . . . . . . . 14 |- ((Lim A /\ y (_ A) -> (A.z e. A E.w e. y z (_ w -> (A (_ U.y /\ U.y (_ A)))
25		eqss 1516	. . . . . . . . . . . . . 14 |- (A = U.y <-> (A (_ U.y /\ U.y (_ A))
26	24, 25	syl6ibr 186	. . . . . . . . . . . . 13 |- ((Lim A /\ y (_ A) -> (A.z e. A E.w e. y z (_ w -> A = U.y))
27	26	exp 291	. . . . . . . . . . . 12 |- (Lim A -> (y (_ A -> (A.z e. A E.w e. y z (_ w -> A = U.y)))
28	27	imdistand 342	. . . . . . . . . . 11 |- (Lim A -> ((y (_ A /\ A.z e. A E.w e. y z (_ w) -> (y (_ A /\ A = U.y)))
29	28	anim2d 433	. . . . . . . . . 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))))
30	29	19.22dv 947	. . . . . . . . 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))))
31	30	19.21aiv 943	. . . . . . . 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))))
32		ss2ab 1551	. . . . . . . 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))))
33	31, 32	sylibr 175	. . . . . . 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))})
34		intss 1983	. . . . . . 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))})
35	33, 34	syl 12	. . . . . 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))})
36	35	adantl 305	. . . . 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))})
37		limelon 2286	. . . . . 6 |- ((A e. V /\ Lim A) -> A e. On)
38		cfval 3701	. . . . . 6 |- (A e. On -> (cf` A) = |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A.z e. A E.w e. y z (_ w))})
39	37, 38	syl 12	. . . . 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))})
40	36, 39	sseqtr4d 1537	. . . 4 |- ((A e. V /\ Lim A) -> |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} (_ (cf` A))
41		cfub 3703	. . . . 5 |- (cf` A) (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A (_ U.y))}
42		eqimss 1548	. . . . . . . . . 10 |- (A = U.y -> A (_ U.y)
43	42	anim2i 270	. . . . . . . . 9 |- ((y (_ A /\ A = U.y) -> (y (_ A /\ A (_ U.y))
44	43	anim2i 270	. . . . . . . 8 |- ((x = (card` y) /\ (y (_ A /\ A = U.y)) -> (x = (card` y) /\ (y (_ A /\ A (_ U.y)))
45	44	19.22i 723	. . . . . . 7 |- (E.y(x = (card` y) /\ (y (_ A /\ A = U.y)) -> E.y(x = (card` y) /\ (y (_ A /\ A (_ U.y)))
46	45	ss2abi 1552	. . . . . 6 |- {x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))} (_ {x | E.y(x = (card` y) /\ (y (_ A /\ A (_ U.y))}
47		intss 1983	. . . . . 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))})
48	46, 47	ax-mp 6	. . . . 5 |- |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A (_ U.y))} (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))}
49	41, 48	sstri 1512	. . . 4 |- (cf` A) (_ |^|{x | E.y(x = (card` y) /\ (y (_ A /\ A = U.y))}
50	40, 49	jctil 240	. . 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)))
51		eqss 1516	. . 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)))
52	50, 51	sylibr 175	. 2 |- ((A e. V /\ Lim A) -> (cf` A) = |^|{x | E.y(x = (card` y)