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

Metamath Proof Explorer

Theorem limom

Description: Omega is a limit ordinal. Theorem 2.8 of BellMachover p. 473. Theorem 1.23 of Schloeder p. 4. 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 ω