Metamath Proof Explorer

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 = ⋃ A
2 1 simp1bi ⊢ Lim ⁡ A → Ord ⁡ A