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

Metamath Proof Explorer

Theorem limomss

Description: The class of natural numbers is a subclass of any (infinite) limit ordinal. Exercise 1 of TakeutiZaring p. 44. Remarkably, our proof does not require the Axiom of Infinity. (Contributed by NM, 30-Oct-2003)

Ref Expression
Assertion limomss ( Lim 𝐴 → ω ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 limord ⊢ ( Lim 𝐴 → Ord 𝐴 )
2 ordeleqon ⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
3 elom ⊢ ( 𝑥 ∈ ω ↔ ( 𝑥 ∈ On ∧ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) ) )
4 3 simprbi ⊢ ( 𝑥 ∈ ω → ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) )
5 limeq ⊢ ( 𝑦 = 𝐴 → ( Lim 𝑦 ↔ Lim 𝐴 ) )
6 eleq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴 ) )
7 5 6 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) ↔ ( Lim 𝐴 → 𝑥 ∈ 𝐴 ) ) )
8 7 spcgv ⊢ ( 𝐴 ∈ On → ( ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) → ( Lim 𝐴 → 𝑥 ∈ 𝐴 ) ) )
9 4 8 syl5 ⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ ω → ( Lim 𝐴 → 𝑥 ∈ 𝐴 ) ) )
10 9 com23 ⊢ ( 𝐴 ∈ On → ( Lim 𝐴 → ( 𝑥 ∈ ω → 𝑥 ∈ 𝐴 ) ) )
11 10 imp ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( 𝑥 ∈ ω → 𝑥 ∈ 𝐴 ) )
12 11 ssrdv ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ω ⊆ 𝐴 )
13 12 ex ⊢ ( 𝐴 ∈ On → ( Lim 𝐴 → ω ⊆ 𝐴 ) )
14 omsson ⊢ ω ⊆ On
15 sseq2 ⊢ ( 𝐴 = On → ( ω ⊆ 𝐴 ↔ ω ⊆ On ) )
16 14 15 mpbiri ⊢ ( 𝐴 = On → ω ⊆ 𝐴 )
17 16 a1d ⊢ ( 𝐴 = On → ( Lim 𝐴 → ω ⊆ 𝐴 ) )
18 13 17 jaoi ⊢ ( ( 𝐴 ∈ On ∨ 𝐴 = On ) → ( Lim 𝐴 → ω ⊆ 𝐴 ) )
19 2 18 sylbi ⊢ ( Ord 𝐴 → ( Lim 𝐴 → ω ⊆ 𝐴 ) )
20 1 19 mpcom ⊢ ( Lim 𝐴 → ω ⊆ 𝐴 )