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 𝐴 → ω ⊆ 𝐴 )