Theorem limord

Description: A limit ordinal is ordinal. (Contributed by NM, 4-May-1995)

	Ref	Expression
Assertion	limord	|- ( Lim A -> Ord A )

Proof

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