This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssnlim

Description: An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of TakeutiZaring p. 42. (Contributed by NM, 2-Nov-2004)

Ref Expression
Assertion ssnlim ( ( Ord 𝐴 ∧ 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ) → 𝐴 ⊆ ω )

Proof

Step Hyp Ref Expression
1 limom ⊢ Lim ω
2 ssel ⊢ ( 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } → ( ω ∈ 𝐴 → ω ∈ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ) )
3 limeq ⊢ ( 𝑥 = ω → ( Lim 𝑥 ↔ Lim ω ) )
4 3 notbid ⊢ ( 𝑥 = ω → ( ¬ Lim 𝑥 ↔ ¬ Lim ω ) )
5 4 elrab ⊢ ( ω ∈ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ↔ ( ω ∈ On ∧ ¬ Lim ω ) )
6 5 simprbi ⊢ ( ω ∈ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } → ¬ Lim ω )
7 2 6 syl6 ⊢ ( 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } → ( ω ∈ 𝐴 → ¬ Lim ω ) )
8 1 7 mt2i ⊢ ( 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } → ¬ ω ∈ 𝐴 )
9 8 adantl ⊢ ( ( Ord 𝐴 ∧ 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ) → ¬ ω ∈ 𝐴 )
10 ordom ⊢ Ord ω
11 ordtri1 ⊢ ( ( Ord 𝐴 ∧ Ord ω ) → ( 𝐴 ⊆ ω ↔ ¬ ω ∈ 𝐴 ) )
12 10 11 mpan2 ⊢ ( Ord 𝐴 → ( 𝐴 ⊆ ω ↔ ¬ ω ∈ 𝐴 ) )
13 12 adantr ⊢ ( ( Ord 𝐴 ∧ 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ) → ( 𝐴 ⊆ ω ↔ ¬ ω ∈ 𝐴 ) )
14 9 13 mpbird ⊢ ( ( Ord 𝐴 ∧ 𝐴 ⊆ { 𝑥 ∈ On ∣ ¬ Lim 𝑥 } ) → 𝐴 ⊆ ω )