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 _om

Proof

Step Hyp Ref Expression
1 ordom 
 |-  Ord _om
2 ordeleqon 
 |-  ( Ord _om <-> ( _om e. On \/ _om = On ) )
3 ordirr 
 |-  ( Ord _om -> -. _om e. _om )
4 1 3 ax-mp 
 |-  -. _om e. _om
5 elom 
 |-  ( _om e. _om <-> ( _om e. On /\ A. x ( Lim x -> _om e. x ) ) )
6 5 baib 
 |-  ( _om e. On -> ( _om e. _om <-> A. x ( Lim x -> _om e. x ) ) )
7 4 6 mtbii 
 |-  ( _om e. On -> -. A. x ( Lim x -> _om e. x ) )
8 limomss 
 |-  ( Lim x -> _om C_ x )
9 limord 
 |-  ( Lim x -> Ord x )
10 ordsseleq 
 |-  ( ( Ord _om /\ Ord x ) -> ( _om C_ x <-> ( _om e. x \/ _om = x ) ) )
11 1 9 10 sylancr 
 |-  ( Lim x -> ( _om C_ x <-> ( _om e. x \/ _om = x ) ) )
12 8 11 mpbid 
 |-  ( Lim x -> ( _om e. x \/ _om = x ) )
13 12 ord 
 |-  ( Lim x -> ( -. _om e. x -> _om = x ) )
14 limeq 
 |-  ( _om = x -> ( Lim _om <-> Lim x ) )
15 14 biimprcd 
 |-  ( Lim x -> ( _om = x -> Lim _om ) )
16 13 15 syld 
 |-  ( Lim x -> ( -. _om e. x -> Lim _om ) )
17 16 con1d 
 |-  ( Lim x -> ( -. Lim _om -> _om e. x ) )
18 17 com12 
 |-  ( -. Lim _om -> ( Lim x -> _om e. x ) )
19 18 alrimiv 
 |-  ( -. Lim _om -> A. x ( Lim x -> _om e. x ) )
20 7 19 nsyl2 
 |-  ( _om e. On -> Lim _om )
21 limon 
 |-  Lim On
22 limeq 
 |-  ( _om = On -> ( Lim _om <-> Lim On ) )
23 21 22 mpbiri 
 |-  ( _om = On -> Lim _om )
24 20 23 jaoi 
 |-  ( ( _om e. On \/ _om = On ) -> Lim _om )
25 2 24 sylbi 
 |-  ( Ord _om -> Lim _om )
26 1 25 ax-mp 
 |-  Lim _om