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 { 𝑥 ∈ On ∣ ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) } = { 𝑥 ∈ On ∣ ¬ Lim 𝑥 }

Proof

Step Hyp Ref Expression
1 eloni ( 𝑥 ∈ On → Ord 𝑥 )
2 dflim3 ( Lim 𝑥 ↔ ( Ord 𝑥 ∧ ¬ ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) )
3 2 baib ( Ord 𝑥 → ( Lim 𝑥 ↔ ¬ ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ) )
4 3 con2bid ( Ord 𝑥 → ( ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ↔ ¬ Lim 𝑥 ) )
5 1 4 syl ( 𝑥 ∈ On → ( ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) ↔ ¬ Lim 𝑥 ) )
6 5 rabbiia { 𝑥 ∈ On ∣ ( 𝑥 = ∅ ∨ ∃ 𝑦 ∈ On 𝑥 = suc 𝑦 ) } = { 𝑥 ∈ On ∣ ¬ Lim 𝑥 }