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