Metamath Proof Explorer

Theorem limuni

Description: A limit ordinal is its own supremum (union). Lemma 2.13 of Schloeder p. 5. (Contributed by NM, 4-May-1995)

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

Proof

Step Hyp Ref Expression
1 df-lim 
 |-  ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
2 1 simp3bi 
 |-  ( Lim A -> A = U. A )