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 𝑥 }