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

Theorem limom 4673
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 4667 . 2  |-  Ord  om
2 ordeleqon 4582 . . 3  |-  ( Ord 
om 
<->  ( om  e.  On  \/  om  =  On ) )
3 ordirr 4412 . . . . . . 7  |-  ( Ord 
om  ->  -.  om  e.  om )
41, 3ax-mp 8 . . . . . 6  |-  -.  om  e.  om
5 elom 4661 . . . . . . 7  |-  ( om  e.  om  <->  ( om  e.  On  /\  A. x
( Lim  x  ->  om  e.  x ) ) )
65baib 871 . . . . . 6  |-  ( om  e.  On  ->  ( om  e.  om  <->  A. x
( Lim  x  ->  om  e.  x ) ) )
74, 6mtbii 293 . . . . 5  |-  ( om  e.  On  ->  -.  A. x ( Lim  x  ->  om  e.  x ) )
8 limomss 4663 . . . . . . . . . . 11  |-  ( Lim  x  ->  om  C_  x
)
9 limord 4453 . . . . . . . . . . . 12  |-  ( Lim  x  ->  Ord  x )
10 ordsseleq 4423 . . . . . . . . . . . 12  |-  ( ( Ord  om  /\  Ord  x )  ->  ( om  C_  x  <->  ( om  e.  x  \/  om  =  x ) ) )
111, 9, 10sylancr 644 . . . . . . . . . . 11  |-  ( Lim  x  ->  ( om  C_  x  <->  ( om  e.  x  \/  om  =  x ) ) )
128, 11mpbid 201 . . . . . . . . . 10  |-  ( Lim  x  ->  ( om  e.  x  \/  om  =  x ) )
1312ord 366 . . . . . . . . 9  |-  ( Lim  x  ->  ( -.  om  e.  x  ->  om  =  x ) )
14 limeq 4406 . . . . . . . . . 10  |-  ( om  =  x  ->  ( Lim  om  <->  Lim  x ) )
1514biimprcd 216 . . . . . . . . 9  |-  ( Lim  x  ->  ( om  =  x  ->  Lim  om ) )
1613, 15syld 40 . . . . . . . 8  |-  ( Lim  x  ->  ( -.  om  e.  x  ->  Lim  om ) )
1716con1d 116 . . . . . . 7  |-  ( Lim  x  ->  ( -.  Lim  om  ->  om  e.  x ) )
1817com12 27 . . . . . 6  |-  ( -. 
Lim  om  ->  ( Lim  x  ->  om  e.  x ) )
1918alrimiv 1619 . . . . 5  |-  ( -. 
Lim  om  ->  A. x
( Lim  x  ->  om  e.  x ) )
207, 19nsyl2 119 . . . 4  |-  ( om  e.  On  ->  Lim  om )
21 limon 4629 . . . . 5  |-  Lim  On
22 limeq 4406 . . . . 5  |-  ( om  =  On  ->  ( Lim  om  <->  Lim  On ) )
2321, 22mpbiri 224 . . . 4  |-  ( om  =  On  ->  Lim  om )
2420, 23jaoi 368 . . 3  |-  ( ( om  e.  On  \/  om  =  On )  ->  Lim  om )
252, 24sylbi 187 . 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 176    \/ wo 357   A.wal 1529    = wceq 1625    e. wcel 1686    C_ wss 3154   Ord word 4393   Oncon0 4394   Lim wlim 4395   omcom 4658
This theorem is referenced by:  peano2b  4674  ssnlim  4676  peano1  4677  onesuc  6531  oaabslem  6643  oaabs2  6645  omabslem  6646  infensuc  7041  infeq5i  7339  elom3  7351  omenps  7357  omensuc  7358  infdifsn  7359  cardlim  7607  r1om  7872  cfom  7892  ominf4  7940  alephom  8209  wunex3  8365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-tr 4116  df-eprel 4307  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659
  Copyright terms: Public domain W3C validator