MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  limom Unicode version

Theorem limom 4802
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.)
Assertion
Ref Expression
limom  |-  Lim  om

Proof of Theorem limom
StepHypRef Expression
1 ordom 4796 . 2  |-  Ord  om
2 ordeleqon 4711 . . 3  |-  ( Ord 
om 
<->  ( om  e.  On  \/  om  =  On ) )
3 ordirr 4542 . . . . . . 7  |-  ( Ord 
om  ->  -.  om  e.  om )
41, 3ax-mp 8 . . . . . 6  |-  -.  om  e.  om
5 elom 4790 . . . . . . 7  |-  ( om  e.  om  <->  ( om  e.  On  /\  A. x
( Lim  x  ->  om  e.  x ) ) )
65baib 872 . . . . . 6  |-  ( om  e.  On  ->  ( om  e.  om  <->  A. x
( Lim  x  ->  om  e.  x ) ) )
74, 6mtbii 294 . . . . 5  |-  ( om  e.  On  ->  -.  A. x ( Lim  x  ->  om  e.  x ) )
8 limomss 4792 . . . . . . . . . . 11  |-  ( Lim  x  ->  om  C_  x
)
9 limord 4583 . . . . . . . . . . . 12  |-  ( Lim  x  ->  Ord  x )
10 ordsseleq 4553 . . . . . . . . . . . 12  |-  ( ( Ord  om  /\  Ord  x )  ->  ( om  C_  x  <->  ( om  e.  x  \/  om  =  x ) ) )
111, 9, 10sylancr 645 . . . . . . . . . . 11  |-  ( Lim  x  ->  ( om  C_  x  <->  ( om  e.  x  \/  om  =  x ) ) )
128, 11mpbid 202 . . . . . . . . . 10  |-  ( Lim  x  ->  ( om  e.  x  \/  om  =  x ) )
1312ord 367 . . . . . . . . 9  |-  ( Lim  x  ->  ( -.  om  e.  x  ->  om  =  x ) )
14 limeq 4536 . . . . . . . . . 10  |-  ( om  =  x  ->  ( Lim  om  <->  Lim  x ) )
1514biimprcd 217 . . . . . . . . 9  |-  ( Lim  x  ->  ( om  =  x  ->  Lim  om ) )
1613, 15syld 42 . . . . . . . 8  |-  ( Lim  x  ->  ( -.  om  e.  x  ->  Lim  om ) )
1716con1d 118 . . . . . . 7  |-  ( Lim  x  ->  ( -.  Lim  om  ->  om  e.  x ) )
1817com12 29 . . . . . 6  |-  ( -. 
Lim  om  ->  ( Lim  x  ->  om  e.  x ) )
1918alrimiv 1638 . . . . 5  |-  ( -. 
Lim  om  ->  A. x
( Lim  x  ->  om  e.  x ) )
207, 19nsyl2 121 . . . 4  |-  ( om  e.  On  ->  Lim  om )
21 limon 4758 . . . . 5  |-  Lim  On
22 limeq 4536 . . . . 5  |-  ( om  =  On  ->  ( Lim  om  <->  Lim  On ) )
2321, 22mpbiri 225 . . . 4  |-  ( om  =  On  ->  Lim  om )
2420, 23jaoi 369 . . 3  |-  ( ( om  e.  On  \/  om  =  On )  ->  Lim  om )
252, 24sylbi 188 . 2  |-  ( Ord 
om  ->  Lim  om )
261, 25ax-mp 8 1  |-  Lim  om
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358   A.wal 1546    = wceq 1649    e. wcel 1717    C_ wss 3265   Ord word 4523   Oncon0 4524   Lim wlim 4525   omcom 4787
This theorem is referenced by:  peano2b  4803  ssnlim  4805  peano1  4806  onesuc  6712  oaabslem  6824  oaabs2  6826  omabslem  6827  infensuc  7223  infeq5i  7526  elom3  7538  omenps  7544  omensuc  7545  infdifsn  7546  cardlim  7794  r1om  8059  cfom  8079  ominf4  8127  alephom  8395  wunex3  8551
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346  ax-un 4643
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-sbc 3107  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-tr 4246  df-eprel 4437  df-po 4446  df-so 4447  df-fr 4484  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530  df-om 4788
  Copyright terms: Public domain W3C validator