Theorem cflim 6057

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 C_ A /\ A = U.y))})

Distinct variable group:   x,y,A

Proof of Theorem cflim

Step	Hyp	Ref	Expression
1		limsuc 3933	. . . . . . . . . . . . . . . . . . 19 |- (Lim A -> (v e. A <-> suc v e. A))
2	1	biimpd 170	. . . . . . . . . . . . . . . . . 18 |- (Lim A -> (v e. A -> suc v e. A))
3		sseq1 2637	. . . . . . . . . . . . . . . . . . . . 21 |- (z = suc v -> (z C_ w <-> suc v C_ w))
4	3	rexbidv 2124	. . . . . . . . . . . . . . . . . . . 20 |- (z = suc v -> (E.w e. y z C_ w <-> E.w e. y suc v C_ w))
5	4	rcla4v 2376	. . . . . . . . . . . . . . . . . . 19 |- (suc v e. A -> (A.z e. A E.w e. y z C_ w -> E.w e. y suc v C_ w))
6		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- v e. _V
7		sucssel 3763	. . . . . . . . . . . . . . . . . . . . . 22 |- (v e. _V -> (suc v C_ w -> v e. w))
8	6, 7	ax-mp 7	. . . . . . . . . . . . . . . . . . . . 21 |- (suc v C_ w -> v e. w)
9	8	reximi 2198	. . . . . . . . . . . . . . . . . . . 20 |- (E.w e. y suc v C_ w -> E.w e. y v e. w)
10		eluni2 3181	. . . . . . . . . . . . . . . . . . . 20 |- (v e. U.y <-> E.w e. y v e. w)
11	9, 10	sylibr 217	. . . . . . . . . . . . . . . . . . 19 |- (E.w e. y suc v C_ w -> v e. U.y)
12	5, 11	syl6com 64	. . . . . . . . . . . . . . . . . 18 |- (A.z e. A E.w e. y z C_ w -> (suc v e. A -> v e. U.y))
13	2, 12	syl9 71	. . . . . . . . . . . . . . . . 17 |- (Lim A -> (A.z e. A E.w e. y z C_ w -> (v e. A -> v e. U.y)))
14	13	r19.21adv 2181	. . . . . . . . . . . . . . . 16 |- (Lim A -> (A.z e. A E.w e. y z C_ w -> A.v e. A v e. U.y))
15		dfss3 2611	. . . . . . . . . . . . . . . 16 |- (A C_ U.y <-> A.v e. A v e. U.y)
16	14, 15	syl6ibr 230	. . . . . . . . . . . . . . 15 |- (Lim A -> (A.z e. A E.w e. y z C_ w -> A C_ U.y))
17	16	adantr 425	. . . . . . . . . . . . . 14 |- ((Lim A /\ y C_ A) -> (A.z e. A E.w e. y z C_ w -> A C_ U.y))
18		limuni 3724	. . . . . . . . . . . . . . . . 17 |- (Lim A -> A = U.A)
19	18	sseq2d 2645	. . . . . . . . . . . . . . . 16 |- (Lim A -> (U.y C_ A <-> U.y C_ U.A))
20		uniss 3199	. . . . . . . . . . . . . . . 16 |- (y C_ A -> U.y C_ U.A)
21	19, 20	syl5bir 227	. . . . . . . . . . . . . . 15 |- (Lim A -> (y C_ A -> U.y C_ A))
22	21	imp 377	. . . . . . . . . . . . . 14 |- ((Lim A /\ y C_ A) -> U.y C_ A)
23	17, 22	jctird 663	. . . . . . . . . . . . 13 |- ((Lim A /\ y C_ A) -> (A.z e. A E.w e. y z C_ w -> (A C_ U.y /\ U.y C_ A)))
24		eqss 2631	. . . . . . . . . . . . 13 |- (A = U.y <-> (A C_ U.y /\ U.y C_ A))
25	23, 24	syl6ibr 230	. . . . . . . . . . . 12 |- ((Lim A /\ y C_ A) -> (A.z e. A E.w e. y z C_ w -> A = U.y))
26	25	ex 402	. . . . . . . . . . 11 |- (Lim A -> (y C_ A -> (A.z e. A E.w e. y z C_ w -> A = U.y)))
27	26	imdistand 493	. . . . . . . . . 10 |- (Lim A -> ((y C_ A /\ A.z e. A E.w e. y z C_ w) -> (y C_ A /\ A = U.y)))
28	27	anim2d 620	. . . . . . . . 9 |- (Lim A -> ((x = (card` y) /\ (y C_ A /\ A.z e. A E.w e. y z C_ w)) -> (x = (card` y) /\ (y C_ A /\ A = U.y))))
29	28	eximdv 1669	. . . . . . . 8 |- (Lim A -> (E.y(x = (card` y) /\ (y C_ A /\ A.z e. A E.w e. y z C_ w)) -> E.y(x = (card` y) /\ (y C_ A /\ A = U.y))))
30	29	ss2abdv 2680	. . . . . . 7 |- (Lim A -> {x | E.y(x = (card` y) /\ (y C_ A /\ A.z e. A E.w e. y z C_ w))} C_ {x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))})
31		intss 3239	. . . . . . 7 |- ({x | E.y(x = (card` y) /\ (y C_ A /\ A.z e. A E.w e. y z C_ w))} C_ {x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} -> |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} C_ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A.z e. A E.w e. y z C_ w))})
32	30, 31	syl 12	. . . . . 6 |- (Lim A -> |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} C_ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A.z e. A E.w e. y z C_ w))})
33	32	adantl 424	. . . . 5 |- ((A e. _V /\ Lim A) -> |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} C_ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A.z e. A E.w e. y z C_ w))})
34		limelon 3727	. . . . . 6 |- ((A e. _V /\ Lim A) -> A e. On)
35		cfval 6054	. . . . . 6 |- (A e. On -> (cf` A) = |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A.z e. A E.w e. y z C_ w))})
36	34, 35	syl 12	. . . . 5 |- ((A e. _V /\ Lim A) -> (cf` A) = |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A.z e. A E.w e. y z C_ w))})
37	33, 36	sseqtr4d 2654	. . . 4 |- ((A e. _V /\ Lim A) -> |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} C_ (cf` A))
38		cfub 6056	. . . . 5 |- (cf` A) C_ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A C_ U.y))}
39		eqimss 2665	. . . . . . . . . 10 |- (A = U.y -> A C_ U.y)
40	39	anim2i 362	. . . . . . . . 9 |- ((y C_ A /\ A = U.y) -> (y C_ A /\ A C_ U.y))
41	40	anim2i 362	. . . . . . . 8 |- ((x = (card` y) /\ (y C_ A /\ A = U.y)) -> (x = (card` y) /\ (y C_ A /\ A C_ U.y)))
42	41	eximi 1387	. . . . . . 7 |- (E.y(x = (card` y) /\ (y C_ A /\ A = U.y)) -> E.y(x = (card` y) /\ (y C_ A /\ A C_ U.y)))
43	42	ss2abi 2679	. . . . . 6 |- {x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} C_ {x | E.y(x = (card` y) /\ (y C_ A /\ A C_ U.y))}
44		intss 3239	. . . . . 6 |- ({x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} C_ {x | E.y(x = (card` y) /\ (y C_ A /\ A C_ U.y))} -> |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A C_ U.y))} C_ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))})
45	43, 44	ax-mp 7	. . . . 5 |- |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A C_ U.y))} C_ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))}
46	38, 45	sstri 2626	. . . 4 |- (cf` A) C_ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))}
47	37, 46	jctil 316	. . 3 |- ((A e. _V /\ Lim A) -> ((cf` A) C_ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} /\ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} C_ (cf` A)))
48		eqss 2631	. . 3 |- ((cf` A) = |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} <-> ((cf` A) C_ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} /\ |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))} C_ (cf` A)))
49	47, 48	sylibr 217	. 2 |- ((A e. _V /\ Lim A) -> (cf` A) = |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))})
50		elisset 2299	. 2 |- (A e. B -> A e. _V)
51	49, 50	sylan 497	1 |- ((A e. B /\ Lim A) -> (cf` A) = |^|{x | E.y(x = (card` y) /\ (y C_ A /\ A = U.y))})

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  U.cuni 3177  |^|cint 3214  Oncon0 3657  Lim wlim 3658  suc csuc 3659  ` cfv 3998  cardccrd 5859  cfccf 5861

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-cf 5864

Copyright terms: Public domain