Theorem limom

Description: Omega is a limit ordinal. Theorem 2.8 of BellMachover p. 473. Our proof, however, does not require the Axiom of Infinity. (Contributed by NM, 26-Mar-1995) (Proof shortened by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Assertion	limom	⊢ Lim ω

Proof

Step	Hyp	Ref	Expression
1		ordom	⊢ Ord ω
2		ordeleqon	⊢ ( Ord ω ↔ ( ω ∈ On ∨ ω = On ) )
3		ordirr	⊢ ( Ord ω → ¬ ω ∈ ω )
4	1 3	ax-mp	⊢ ¬ ω ∈ ω
5		elom	⊢ ( ω ∈ ω ↔ ( ω ∈ On ∧ ∀ 𝑥 ( Lim 𝑥 → ω ∈ 𝑥 ) ) )
6	5	baib	⊢ ( ω ∈ On → ( ω ∈ ω ↔ ∀ 𝑥 ( Lim 𝑥 → ω ∈ 𝑥 ) ) )
7	4 6	mtbii	⊢ ( ω ∈ On → ¬ ∀ 𝑥 ( Lim 𝑥 → ω ∈ 𝑥 ) )
8		limomss	⊢ ( Lim 𝑥 → ω ⊆ 𝑥 )
9		limord	⊢ ( Lim 𝑥 → Ord 𝑥 )
10		ordsseleq	⊢ ( ( Ord ω ∧ Ord 𝑥 ) → ( ω ⊆ 𝑥 ↔ ( ω ∈ 𝑥 ∨ ω = 𝑥 ) ) )
11	1 9 10	sylancr	⊢ ( Lim 𝑥 → ( ω ⊆ 𝑥 ↔ ( ω ∈ 𝑥 ∨ ω = 𝑥 ) ) )
12	8 11	mpbid	⊢ ( Lim 𝑥 → ( ω ∈ 𝑥 ∨ ω = 𝑥 ) )
13	12	ord	⊢ ( Lim 𝑥 → ( ¬ ω ∈ 𝑥 → ω = 𝑥 ) )
14		limeq	⊢ ( ω = 𝑥 → ( Lim ω ↔ Lim 𝑥 ) )
15	14	biimprcd	⊢ ( Lim 𝑥 → ( ω = 𝑥 → Lim ω ) )
16	13 15	syld	⊢ ( Lim 𝑥 → ( ¬ ω ∈ 𝑥 → Lim ω ) )
17	16	con1d	⊢ ( Lim 𝑥 → ( ¬ Lim ω → ω ∈ 𝑥 ) )
18	17	com12	⊢ ( ¬ Lim ω → ( Lim 𝑥 → ω ∈ 𝑥 ) )
19	18	alrimiv	⊢ ( ¬ Lim ω → ∀ 𝑥 ( Lim 𝑥 → ω ∈ 𝑥 ) )
20	7 19	nsyl2	⊢ ( ω ∈ On → Lim ω )
21		limon	⊢ Lim On
22		limeq	⊢ ( ω = On → ( Lim ω ↔ Lim On ) )
23	21 22	mpbiri	⊢ ( ω = On → Lim ω )
24	20 23	jaoi	⊢ ( ( ω ∈ On ∨ ω = On ) → Lim ω )
25	2 24	sylbi	⊢ ( Ord ω → Lim ω )
26	1 25	ax-mp	⊢ Lim ω