Metamath Proof Explorer

Theorem limuni2

Description: The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006)

Ref Expression
Assertion limuni2 
|- ( Lim A -> Lim U. A )

Proof

Step Hyp Ref Expression
1 limuni 
 |-  ( Lim A -> A = U. A )
2 limeq 
 |-  ( A = U. A -> ( Lim A <-> Lim U. A ) )
3 1 2 syl 
 |-  ( Lim A -> ( Lim A <-> Lim U. A ) )
4 3 ibi 
 |-  ( Lim A -> Lim U. A )