Theorem omsublim 5887

Description: An infinite initial ordinal is a limit ordinal. (Contributed by Jeff Hankins, 29-Oct-2009.)

Assertion

Ref	Expression
omsublim	|- (A e. On -> Lim (aleph` A))

Proof of Theorem omsublim

Step	Hyp	Ref	Expression
1		fveq2 4681	. . 3 |- (x = (/) -> (aleph` x) = (aleph` (/)))
2		limeq 3669	. . 3 |- ((aleph` x) = (aleph` (/)) -> (Lim (aleph` x) <-> Lim (aleph` (/))))
3	1, 2	syl 12	. 2 |- (x = (/) -> (Lim (aleph` x) <-> Lim (aleph` (/))))
4		fveq2 4681	. . 3 |- (x = y -> (aleph` x) = (aleph` y))
5		limeq 3669	. . 3 |- ((aleph` x) = (aleph` y) -> (Lim (aleph` x) <-> Lim (aleph` y)))
6	4, 5	syl 12	. 2 |- (x = y -> (Lim (aleph` x) <-> Lim (aleph` y)))
7		fveq2 4681	. . 3 |- (x = suc y -> (aleph` x) = (aleph` suc y))
8		limeq 3669	. . 3 |- ((aleph` x) = (aleph` suc y) -> (Lim (aleph` x) <-> Lim (aleph` suc y)))
9	7, 8	syl 12	. 2 |- (x = suc y -> (Lim (aleph` x) <-> Lim (aleph` suc y)))
10		fveq2 4681	. . 3 |- (x = A -> (aleph` x) = (aleph` A))
11		limeq 3669	. . 3 |- ((aleph` x) = (aleph` A) -> (Lim (aleph` x) <-> Lim (aleph` A)))
12	10, 11	syl 12	. 2 |- (x = A -> (Lim (aleph` x) <-> Lim (aleph` A)))
13		limom 3967	. . 3 |- Lim om
14		aleph0 5874	. . . 4 |- (aleph` (/)) = om
15		limeq 3669	. . . 4 |- ((aleph` (/)) = om -> (Lim (aleph` (/)) <-> Lim om))
16	14, 15	ax-mp 7	. . 3 |- (Lim (aleph` (/)) <-> Lim om)
17	13, 16	mpbir 207	. 2 |- Lim (aleph` (/))
18		alephon 5876	. . . . . . 7 |- (aleph` suc y) e. On
19		eloni 3667	. . . . . . 7 |- ((aleph` suc y) e. On -> Ord (aleph` suc y))
20	18, 19	ax-mp 7	. . . . . 6 |- Ord (aleph` suc y)
21	20	a1i 8	. . . . 5 |- (y e. On -> Ord (aleph` suc y))
22		0elon 3716	. . . . . . 7 |- (/) e. On
23		0ex 3446	. . . . . . . 8 |- (/) e. _V
24		0ss 2900	. . . . . . . 8 |- (/) C_ (aleph` y)
25		ssdomg 5467	. . . . . . . 8 |- ((/) e. _V -> ((/) C_ (aleph` y) -> (/) ~<_ (aleph` y)))
26	23, 24, 25	mp2 54	. . . . . . 7 |- (/) ~<_ (aleph` y)
27	22, 26	pm3.2i 307	. . . . . 6 |- ((/) e. On /\ (/) ~<_ (aleph` y))
28		omsubsuc2 5878	. . . . . . . 8 |- (y e. On -> (aleph` suc y) = {x e. On | x ~<_ (aleph` y)})
29	28	eleq2d 1964	. . . . . . 7 |- (y e. On -> ((/) e. (aleph` suc y) <-> (/) e. {x e. On | x ~<_ (aleph` y)}))
30		breq1 3341	. . . . . . . 8 |- (x = (/) -> (x ~<_ (aleph` y) <-> (/) ~<_ (aleph` y)))
31	30	elrab 2414	. . . . . . 7 |- ((/) e. {x e. On | x ~<_ (aleph` y)} <-> ((/) e. On /\ (/) ~<_ (aleph` y)))
32	29, 31	syl6rbb 596	. . . . . 6 |- (y e. On -> (((/) e. On /\ (/) ~<_ (aleph` y)) <-> (/) e. (aleph` suc y)))
33	27, 32	mpbii 210	. . . . 5 |- (y e. On -> (/) e. (aleph` suc y))
34		suceloni 3894	. . . . . . . . . 10 |- (x e. On -> suc x e. On)
35	34	adantr 425	. . . . . . . . 9 |- ((x e. On /\ x ~<_ (aleph` y)) -> suc x e. On)
36	35	a1i 8	. . . . . . . 8 |- (y e. On -> ((x e. On /\ x ~<_ (aleph` y)) -> suc x e. On))
37		eloni 3667	. . . . . . . . . . . . 13 |- (x e. On -> Ord x)
38		ordom 3960	. . . . . . . . . . . . . 14 |- Ord om
39		ordtri2or 3766	. . . . . . . . . . . . . 14 |- ((Ord x /\ Ord om) -> (x e. om \/ om C_ x))
40	38, 39	mpan2 760	. . . . . . . . . . . . 13 |- (Ord x -> (x e. om \/ om C_ x))
41	37, 40	syl 12	. . . . . . . . . . . 12 |- (x e. On -> (x e. om \/ om C_ x))
42	41	adantl 424	. . . . . . . . . . 11 |- ((y e. On /\ x e. On) -> (x e. om \/ om C_ x))
43		peano2 3972	. . . . . . . . . . . . . . . . 17 |- (x e. om -> suc x e. om)
44	43	adantl 424	. . . . . . . . . . . . . . . 16 |- ((y e. On /\ x e. om) -> suc x e. om)
45		omelon 5736	. . . . . . . . . . . . . . . . . . 19 |- om e. On
46		onelss 3705	. . . . . . . . . . . . . . . . . . 19 |- (om e. On -> (suc x e. om -> suc x C_ om))
47	45, 46	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- (suc x e. om -> suc x C_ om)
48	43, 47	syl 12	. . . . . . . . . . . . . . . . 17 |- (x e. om -> suc x C_ om)
49		0ss 2900	. . . . . . . . . . . . . . . . . . 19 |- (/) C_ y
50		omsubss 5884	. . . . . . . . . . . . . . . . . . . 20 |- (((/) e. On /\ y e. On) -> ((/) C_ y <-> (aleph` (/)) C_ (aleph` y)))
51	22, 50	mpan 759	. . . . . . . . . . . . . . . . . . 19 |- (y e. On -> ((/) C_ y <-> (aleph` (/)) C_ (aleph` y)))
52	49, 51	mpbii 210	. . . . . . . . . . . . . . . . . 18 |- (y e. On -> (aleph` (/)) C_ (aleph` y))
53	52, 14	syl5ssr 2662	. . . . . . . . . . . . . . . . 17 |- (y e. On -> om C_ (aleph` y))
54	48, 53	sylan9ssr 2630	. . . . . . . . . . . . . . . 16 |- ((y e. On /\ x e. om) -> suc x C_ (aleph` y))
55		ssdomg 5467	. . . . . . . . . . . . . . . 16 |- (suc x e. om -> (suc x C_ (aleph` y) -> suc x ~<_ (aleph` y)))
56	44, 54, 55	sylc 83	. . . . . . . . . . . . . . 15 |- ((y e. On /\ x e. om) -> suc x ~<_ (aleph` y))
57	56	ex 402	. . . . . . . . . . . . . 14 |- (y e. On -> (x e. om -> suc x ~<_ (aleph` y)))
58	57	a1dd 53	. . . . . . . . . . . . 13 |- (y e. On -> (x e. om -> (x ~<_ (aleph` y) -> suc x ~<_ (aleph` y))))
59	58	adantr 425	. . . . . . . . . . . 12 |- ((y e. On /\ x e. On) -> (x e. om -> (x ~<_ (aleph` y) -> suc x ~<_ (aleph` y))))
60		infensuc 5745	. . . . . . . . . . . . . . . 16 |- ((x e. On /\ om C_ x) -> x ~~ suc x)
61	60	ad2ant2lr 446	. . . . . . . . . . . . . . 15 |- (((y e. On /\ x e. On) /\ (om C_ x /\ x ~<_ (aleph` y))) -> x ~~ suc x)
62		visset 2295	. . . . . . . . . . . . . . . . 17 |- x e. _V
63	62	sucex 3892	. . . . . . . . . . . . . . . 16 |- suc x e. _V
64		ensymg 5470	. . . . . . . . . . . . . . . 16 |- (suc x e. _V -> (x ~~ suc x -> suc x ~~ x))
65	63, 64	ax-mp 7	. . . . . . . . . . . . . . 15 |- (x ~~ suc x -> suc x ~~ x)
66	61, 65	syl 12	. . . . . . . . . . . . . 14 |- (((y e. On /\ x e. On) /\ (om C_ x /\ x ~<_ (aleph` y))) -> suc x ~~ x)
67		simprr 451	. . . . . . . . . . . . . 14 |- (((y e. On /\ x e. On) /\ (om C_ x /\ x ~<_ (aleph` y))) -> x ~<_ (aleph` y))
68		endomtr 5479	. . . . . . . . . . . . . 14 |- ((suc x ~~ x /\ x ~<_ (aleph` y)) -> suc x ~<_ (aleph` y))
69	66, 67, 68	syl11anc 524	. . . . . . . . . . . . 13 |- (((y e. On /\ x e. On) /\ (om C_ x /\ x ~<_ (aleph` y))) -> suc x ~<_ (aleph` y))
70	69	exp32 408	. . . . . . . . . . . 12 |- ((y e. On /\ x e. On) -> (om C_ x -> (x ~<_ (aleph` y) -> suc x ~<_ (aleph` y))))
71	59, 70	jaod 469	. . . . . . . . . . 11 |- ((y e. On /\ x e. On) -> ((x e. om \/ om C_ x) -> (x ~<_ (aleph` y) -> suc x ~<_ (aleph` y))))
72	42, 71	mpd 29	. . . . . . . . . 10 |- ((y e. On /\ x e. On) -> (x ~<_ (aleph` y) -> suc x ~<_ (aleph` y)))
73	72	ex 402	. . . . . . . . 9 |- (y e. On -> (x e. On -> (x ~<_ (aleph` y) -> suc x ~<_ (aleph` y))))
74	73	imp3a 388	. . . . . . . 8 |- (y e. On -> ((x e. On /\ x ~<_ (aleph` y)) -> suc x ~<_ (aleph` y)))
75	36, 74	jcad 661	. . . . . . 7 |- (y e. On -> ((x e. On /\ x ~<_ (aleph` y)) -> (suc x e. On /\ suc x ~<_ (aleph` y))))
76		omsubsuc2 5878	. . . . . . . . 9 |- (y e. On -> (aleph` suc y) = {z e. On | z ~<_ (aleph` y)})
77	76	eleq2d 1964	. . . . . . . 8 |- (y e. On -> (x e. (aleph` suc y) <-> x e. {z e. On | z ~<_ (aleph` y)}))
78		breq1 3341	. . . . . . . . 9 |- (z = x -> (z ~<_ (aleph` y) <-> x ~<_ (aleph` y)))
79	78	elrab 2414	. . . . . . . 8 |- (x e. {z e. On | z ~<_ (aleph` y)} <-> (x e. On /\ x ~<_ (aleph` y)))
80	77, 79	syl6bb 595	. . . . . . 7 |- (y e. On -> (x e. (aleph` suc y) <-> (x e. On /\ x ~<_ (aleph` y))))
81	76	eleq2d 1964	. . . . . . . 8 |- (y e. On -> (suc x e. (aleph` suc y) <-> suc x e. {z e. On | z ~<_ (aleph` y)}))
82		breq1 3341	. . . . . . . . 9 |- (z = suc x -> (z ~<_ (aleph` y) <-> suc x ~<_ (aleph` y)))
83	82	elrab 2414	. . . . . . . 8 |- (suc x e. {z e. On | z ~<_ (aleph` y)} <-> (suc x e. On /\ suc x ~<_ (aleph` y)))
84	81, 83	syl6bb 595	. . . . . . 7 |- (y e. On -> (suc x e. (aleph` suc y) <-> (suc x e. On /\ suc x ~<_ (aleph` y))))
85	75, 80, 84	3imtr4d 602	. . . . . 6 |- (y e. On -> (x e. (aleph` suc y) -> suc x e. (aleph` suc y)))
86	85	r19.21aiv 2175	. . . . 5 |- (y e. On -> A.x e. (aleph` suc y)suc x e. (aleph` suc y))
87	21, 33, 86	3jca 1050	. . . 4 |- (y e. On -> (Ord (aleph` suc y) /\ (/) e. (aleph` suc y) /\ A.x e. (aleph` suc y)suc x e. (aleph` suc y)))
88		dflim4 3932	. . . 4 |- (Lim (aleph` suc y) <-> (Ord (aleph` suc y) /\ (/) e. (aleph` suc y) /\ A.x e. (aleph` suc y)suc x e. (aleph` suc y)))
89	87, 88	sylibr 217	. . 3 |- (y e. On -> Lim (aleph` suc y))
90	89	a1d 15	. 2 |- (y e. On -> (Lim (aleph` y) -> Lim (aleph` suc y)))
91		0ellim 3726	. . . . . . . . 9 |- (Lim x -> (/) e. x)
92		eqid 1884	. . . . . . . . . 10 |- (aleph` (/)) = (aleph` (/))
93		fveq2 4681	. . . . . . . . . . . 12 |- (z = (/) -> (aleph` z) = (aleph` (/)))
94	93	eqeq2d 1895	. . . . . . . . . . 11 |- (z = (/) -> ((aleph` (/)) = (aleph` z) <-> (aleph` (/)) = (aleph` (/))))
95	94	rcla4ev 2381	. . . . . . . . . 10 |- (((/) e. x /\ (aleph` (/)) = (aleph` (/))) -> E.z e. x (aleph` (/)) = (aleph` z))
96	92, 95	mpan2 760	. . . . . . . . 9 |- ((/) e. x -> E.z e. x (aleph` (/)) = (aleph` z))
97	91, 96	syl 12	. . . . . . . 8 |- (Lim x -> E.z e. x (aleph` (/)) = (aleph` z))
98	97	adantr 425	. . . . . . 7 |- ((Lim x /\ A.y e. x Lim (aleph` y)) -> E.z e. x (aleph` (/)) = (aleph` z))
99		fvex 4689	. . . . . . . 8 |- (aleph` (/)) e. _V
100		eqeq1 1890	. . . . . . . . 9 |- (w = (aleph` (/)) -> (w = (aleph` z) <-> (aleph` (/)) = (aleph` z)))
101	100	rexbidv 2124	. . . . . . . 8 |- (w = (aleph` (/)) -> (E.z e. x w = (aleph` z) <-> E.z e. x (aleph` (/)) = (aleph` z)))
102	99, 101	elab 2403	. . . . . . 7 |- ((aleph` (/)) e. {w | E.z e. x w = (aleph` z)} <-> E.z e. x (aleph` (/)) = (aleph` z))
103	98, 102	sylibr 217	. . . . . 6 |- ((Lim x /\ A.y e. x Lim (aleph` y)) -> (aleph` (/)) e. {w | E.z e. x w = (aleph` z)})
104		ne0i 2881	. . . . . 6 |- ((aleph` (/)) e. {w | E.z e. x w = (aleph` z)} -> {w | E.z e. x w = (aleph` z)} =/= (/))
105	103, 104	syl 12	. . . . 5 |- ((Lim x /\ A.y e. x Lim (aleph` y)) -> {w | E.z e. x w = (aleph` z)} =/= (/))
106		fveq2 4681	. . . . . . . . . . 11 |- (y = z -> (aleph` y) = (aleph` z))
107		limeq 3669	. . . . . . . . . . 11 |- ((aleph` y) = (aleph` z) -> (Lim (aleph` y) <-> Lim (aleph` z)))
108	106, 107	syl 12	. . . . . . . . . 10 |- (y = z -> (Lim (aleph` y) <-> Lim (aleph` z)))
109	108	rcla4cv 2377	. . . . . . . . 9 |- (A.y e. x Lim (aleph` y) -> (z e. x -> Lim (aleph` z)))
110		limeq 3669	. . . . . . . . . . 11 |- (t = (aleph` z) -> (Lim t <-> Lim (aleph` z)))
111	110	biimprcd 173	. . . . . . . . . 10 |- (Lim (aleph` z) -> (t = (aleph` z) -> Lim t))
112	111	a1i 8	. . . . . . . . 9 |- (Lim x -> (Lim (aleph` z) -> (t = (aleph` z) -> Lim t)))
113	109, 112	sylan9r 519	. . . . . . . 8 |- ((Lim x /\ A.y e. x Lim (aleph` y)) -> (z e. x -> (t = (aleph` z) -> Lim t)))
114	113	r19.23adv 2215	. . . . . . 7 |- ((Lim x /\ A.y e. x Lim (aleph` y)) -> (E.z e. x t = (aleph` z) -> Lim t))
115		visset 2295	. . . . . . . 8 |- t e. _V
116		eqeq1 1890	. . . . . . . . 9 |- (w = t -> (w = (aleph` z) <-> t = (aleph` z)))
117	116	rexbidv 2124	. . . . . . . 8 |- (w = t -> (E.z e. x w = (aleph` z) <-> E.z e. x t = (aleph` z)))
118	115, 117	elab 2403	. . . . . . 7 |- (t e. {w | E.z e. x w = (aleph` z)} <-> E.z e. x t = (aleph` z))
119	114, 118	syl5ib 223	. . . . . 6 |- ((Lim x /\ A.y e. x Lim (aleph` y)) -> (t e. {w | E.z e. x w = (aleph` z)} -> Lim t))
120	119	r19.21aiv 2175	. . . . 5 |- ((Lim x /\ A.y e. x Lim (aleph` y)) -> A.t e. {w | E.z e. x w = (aleph` z)}Lim t)
121		limuni3 3936	. . . . 5 |- (({w | E.z e. x w = (aleph` z)} =/= (/) /\ A.t e. {w | E.z e. x w = (aleph` z)}Lim t) -> Lim U.{w | E.z e. x w = (aleph` z)})
122	105, 120, 121	syl11anc 524	. . . 4 |- ((Lim x /\ A.y e. x Lim (aleph` y)) -> Lim U.{w | E.z e. x w = (aleph` z)})
123		alephlim 5875	. . . . . . . 8 |- ((x e. _V /\ Lim x) -> (aleph` x) = U_z e. x (aleph` z))
124	62, 123	mpan 759	. . . . . . 7 |- (Lim x -> (aleph` x) = U_z e. x (aleph` z))
125		fvex 4689	. . . . . . . 8 |- (aleph` z) e. _V
126	125	dfiun2 3285	. . . . . . 7 |- U_z e. x (aleph` z) = U.{w | E.z e. x w = (aleph` z)}
127	124, 126	syl6eq 1944	. . . . . 6 |- (Lim x -> (aleph` x) = U.{w | E.z e. x w = (aleph` z)})
128		limeq 3669	. . . . . 6 |- ((aleph` x) = U.{w | E.z e. x w = (aleph` z)} -> (Lim (aleph` x) <-> Lim U.{w | E.z e. x w = (aleph` z)}))
129	127, 128	syl 12	. . . . 5 |- (Lim x -> (Lim (aleph` x) <-> Lim U.{w | E.z e. x w = (aleph` z)}))
130	129	adantr 425	. . . 4 |- ((Lim x /\ A.y e. x Lim (aleph` y)) -> (Lim (aleph` x) <-> Lim U.{w | E.z e. x w = (aleph` z)}))
131	122, 130	mpbird 213	. . 3 |- ((Lim x /\ A.y e. x Lim (aleph` y)) -> Lim (aleph` x))
132	131	ex 402	. 2 |- (Lim x -> (A.y e. x Lim (aleph` y) -> Lim (aleph` x)))
133	3, 6, 9, 12, 17, 90, 132	tfinds 3942	1 |- (A e. On -> Lim (aleph` A))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  U.cuni 3177  U_ciun 3255   class class class wbr 3338  Ord word 3656  Oncon0 3657  Lim wlim 3658  suc csuc 3659  omcom 3949  ` cfv 3998   ~~ cen 5423   ~<_ cdom 5424  alephcale 5860

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-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

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-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  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-iun 3257  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-om 3950  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-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-iso 4015  df-oprab 4887  df-rdg 5140  df-1o 5177  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-aleph 5863

Copyright terms: Public domain