Metamath Proof Explorer

Theorem limuni3

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

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

Proof

Step Hyp Ref Expression
1 limeq 
 |-  ( x = z -> ( Lim x <-> Lim z ) )
2 1 rspcv 
 |-  ( z e. A -> ( A. x e. A Lim x -> Lim z ) )
3 vex 
 |-  z e. _V
4 limelon 
 |-  ( ( z e. _V /\ Lim z ) -> z e. On )
5 3 4 mpan 
 |-  ( Lim z -> z e. On )
6 2 5 syl6com 
 |-  ( A. x e. A Lim x -> ( z e. A -> z e. On ) )
7 6 ssrdv 
 |-  ( A. x e. A Lim x -> A C_ On )
8 ssorduni 
 |-  ( A C_ On -> Ord U. A )
9 7 8 syl 
 |-  ( A. x e. A Lim x -> Ord U. A )
10 9 adantl 
 |-  ( ( A =/= (/) /\ A. x e. A Lim x ) -> Ord U. A )
11 n0 
 |-  ( A =/= (/) <-> E. z z e. A )
12 0ellim 
 |-  ( Lim z -> (/) e. z )
13 elunii 
 |-  ( ( (/) e. z /\ z e. A ) -> (/) e. U. A )
14 13 expcom 
 |-  ( z e. A -> ( (/) e. z -> (/) e. U. A ) )
15 12 14 syl5 
 |-  ( z e. A -> ( Lim z -> (/) e. U. A ) )
16 2 15 syld 
 |-  ( z e. A -> ( A. x e. A Lim x -> (/) e. U. A ) )
17 16 exlimiv 
 |-  ( E. z z e. A -> ( A. x e. A Lim x -> (/) e. U. A ) )
18 11 17 sylbi 
 |-  ( A =/= (/) -> ( A. x e. A Lim x -> (/) e. U. A ) )
19 18 imp 
 |-  ( ( A =/= (/) /\ A. x e. A Lim x ) -> (/) e. U. A )
20 eluni2 
 |-  ( y e. U. A <-> E. z e. A y e. z )
21 1 rspccv 
 |-  ( A. x e. A Lim x -> ( z e. A -> Lim z ) )
22 limsuc 
 |-  ( Lim z -> ( y e. z <-> suc y e. z ) )
23 22 anbi1d 
 |-  ( Lim z -> ( ( y e. z /\ z e. A ) <-> ( suc y e. z /\ z e. A ) ) )
24 elunii 
 |-  ( ( suc y e. z /\ z e. A ) -> suc y e. U. A )
25 23 24 syl6bi 
 |-  ( Lim z -> ( ( y e. z /\ z e. A ) -> suc y e. U. A ) )
26 25 expd 
 |-  ( Lim z -> ( y e. z -> ( z e. A -> suc y e. U. A ) ) )
27 26 com3r 
 |-  ( z e. A -> ( Lim z -> ( y e. z -> suc y e. U. A ) ) )
28 21 27 sylcom 
 |-  ( A. x e. A Lim x -> ( z e. A -> ( y e. z -> suc y e. U. A ) ) )
29 28 rexlimdv 
 |-  ( A. x e. A Lim x -> ( E. z e. A y e. z -> suc y e. U. A ) )
30 20 29 syl5bi 
 |-  ( A. x e. A Lim x -> ( y e. U. A -> suc y e. U. A ) )
31 30 ralrimiv 
 |-  ( A. x e. A Lim x -> A. y e. U. A suc y e. U. A )
32 31 adantl 
 |-  ( ( A =/= (/) /\ A. x e. A Lim x ) -> A. y e. U. A suc y e. U. A )
33 dflim4 
 |-  ( 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 
 |-  ( ( A =/= (/) /\ A. x e. A Lim x ) -> Lim U. A )