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 ⁡ A → ω ⊆ A

Proof

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