Metamath Proof Explorer

Theorem nlimon

Description: Two ways to express the class of non-limit ordinal numbers. Part of Definition 7.27 of TakeutiZaring p. 42, who use the symbol K_I for this class. (Contributed by NM, 1-Nov-2004)

Ref Expression
Assertion nlimon ⊢ x ∈ On | x = ∅ ∨ ∃ y ∈ On x = suc ⁡ y = x ∈ On | ¬ Lim ⁡ x

Proof

Step Hyp Ref Expression
1 eloni ⊢ x ∈ On → Ord ⁡ x
2 dflim3 ⊢ Lim ⁡ x ↔ Ord ⁡ x ∧ ¬ x = ∅ ∨ ∃ y ∈ On x = suc ⁡ y
3 2 baib ⊢ Ord ⁡ x → Lim ⁡ x ↔ ¬ x = ∅ ∨ ∃ y ∈ On x = suc ⁡ y
4 3 con2bid ⊢ Ord ⁡ x → x = ∅ ∨ ∃ y ∈ On x = suc ⁡ y ↔ ¬ Lim ⁡ x
5 1 4 syl ⊢ x ∈ On → x = ∅ ∨ ∃ y ∈ On x = suc ⁡ y ↔ ¬ Lim ⁡ x
6 5 rabbiia ⊢ x ∈ On | x = ∅ ∨ ∃ y ∈ On x = suc ⁡ y = x ∈ On | ¬ Lim ⁡ x