Theorem limuni3 4791

Description: The union of a nonempty class of limit ordinals is a limit ordinal. (Contributed by NM, 1-Feb-2005.)

Assertion

Ref	Expression
limuni3	|- ( ( A =/= (/) /\ A. x e. A Lim x ) -> Lim U. A )

Distinct variable group:   x, A

Proof of Theorem limuni3

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		limeq 4553	. . . . . . 7 |- ( x = z -> ( Lim x <-> Lim z ) )
2	1	rspcv 3008	. . . . . 6 |- ( z e. A -> ( A. x e. A Lim x -> Lim z ) )
3		vex 2919	. . . . . . 7 |- z e. _V
4		limelon 4604	. . . . . . 7 |- ( ( z e. _V /\ Lim z ) -> z e. On )
5	3, 4	mpan 652	. . . . . 6 |- ( Lim z -> z e. On )
6	2, 5	syl6com 33	. . . . 5 |- ( A. x e. A Lim x -> ( z e. A -> z e. On ) )
7	6	ssrdv 3314	. . . 4 |- ( A. x e. A Lim x -> A C_ On )
8		ssorduni 4725	. . . 4 |- ( A C_ On -> Ord U. A )
9	7, 8	syl 16	. . 3 |- ( A. x e. A Lim x -> Ord U. A )
10	9	adantl 453	. 2 |- ( ( A =/= (/) /\ A. x e. A Lim x ) -> Ord U. A )
11		n0 3597	. . . 4 |- ( A =/= (/) <-> E. z z e. A )
12		0ellim 4603	. . . . . . 7 |- ( Lim z -> (/) e. z )
13		elunii 3980	. . . . . . . 8 |- ( ( (/) e. z /\ z e. A ) -> (/) e. U. A )
14	13	expcom 425	. . . . . . 7 |- ( z e. A -> ( (/) e. z -> (/) e. U. A ) )
15	12, 14	syl5 30	. . . . . 6 |- ( z e. A -> ( Lim z -> (/) e. U. A ) )
16	2, 15	syld 42	. . . . 5 |- ( z e. A -> ( A. x e. A Lim x -> (/) e. U. A ) )
17	16	exlimiv 1641	. . . 4 |- ( E. z z e. A -> ( A. x e. A Lim x -> (/) e. U. A ) )
18	11, 17	sylbi 188	. . 3 |- ( A =/= (/) -> ( A. x e. A Lim x -> (/) e. U. A ) )
19	18	imp 419	. 2 |- ( ( A =/= (/) /\ A. x e. A Lim x ) -> (/) e. U. A )
20		eluni2 3979	. . . . 5 |- ( y e. U. A <-> E. z e. A y e. z )
21	1	rspccv 3009	. . . . . . 7 |- ( A. x e. A Lim x -> ( z e. A -> Lim z ) )
22		limsuc 4788	. . . . . . . . . . 11 |- ( Lim z -> ( y e. z <-> suc y e. z ) )
23	22	anbi1d 686	. . . . . . . . . 10 |- ( Lim z -> ( ( y e. z /\ z e. A ) <-> ( suc y e. z /\ z e. A ) ) )
24		elunii 3980	. . . . . . . . . 10 |- ( ( suc y e. z /\ z e. A ) -> suc y e. U. A )
25	23, 24	syl6bi 220	. . . . . . . . 9 |- ( Lim z -> ( ( y e. z /\ z e. A ) -> suc y e. U. A ) )
26	25	exp3a 426	. . . . . . . 8 |- ( Lim z -> ( y e. z -> ( z e. A -> suc y e. U. A ) ) )
27	26	com3r 75	. . . . . . 7 |- ( z e. A -> ( Lim z -> ( y e. z -> suc y e. U. A ) ) )
28	21, 27	sylcom 27	. . . . . 6 |- ( A. x e. A Lim x -> ( z e. A -> ( y e. z -> suc y e. U. A ) ) )
29	28	rexlimdv 2789	. . . . 5 |- ( A. x e. A Lim x -> ( E. z e. A y e. z -> suc y e. U. A ) )
30	20, 29	syl5bi 209	. . . 4 |- ( A. x e. A Lim x -> ( y e. U. A -> suc y e. U. A ) )
31	30	ralrimiv 2748	. . 3 |- ( A. x e. A Lim x -> A. y e. U. A suc y e. U. A )
32	31	adantl 453	. 2 |- ( ( A =/= (/) /\ A. x e. A Lim x ) -> A. y e. U. A suc y e. U. A )
33		dflim4 4787	. 2 |- ( Lim U. A <-> ( Ord U. A /\ (/) e. U. A /\ A. y e. U. A suc y e. U. A ) )
34	10, 19, 32, 33	syl3anbrc 1138	1 |- ( ( A =/= (/) /\ A. x e. A Lim x ) -> Lim U. A )

Syntax hints:   -> wi 4   /\ wa 359   E.wex 1547   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   C_ wss 3280   (/)c0 3588   U.cuni 3975   Ord word 4540   Oncon0 4541   Lim wlim 4542   suc csuc 4543

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-tr 4263  df-eprel 4454  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547