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

Theorem limom 4670
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 4664 . 2  |-  Ord  om
2 ordeleqon 4579 . . 3  |-  ( Ord 
om 
<->  ( om  e.  On  \/  om  =  On ) )
3 ordirr 4409 . . . . . . 7  |-  ( Ord 
om  ->  -.  om  e.  om )
41, 3ax-mp 8 . . . . . 6  |-  -.  om  e.  om
5 elom 4658 . . . . . . 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 4660 . . . . . . . . . . 11  |-  ( Lim  x  ->  om  C_  x
)
9 limord 4450 . . . . . . . . . . . 12  |-  ( Lim  x  ->  Ord  x )
10 ordsseleq 4420 . . . . . . . . . . . 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 4403 . . . . . . . . . 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 1617 . . . . 5  |-  ( -. 
Lim  om  ->  A. x
( Lim  x  ->  om  e.  x ) )
207, 19nsyl2 119 . . . 4  |-  ( om  e.  On  ->  Lim  om )
21 limon 4626 . . . . 5  |-  Lim  On
22 limeq 4403 . . . . 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 1527    = wceq 1623    e. wcel 1685    C_ wss 3153   Ord word 4390   Oncon0 4391   Lim wlim 4392   omcom 4655
This theorem is referenced by:  peano2b  4671  ssnlim  4673  peano1  4674  onesuc  6525  oaabslem  6637  oaabs2  6639  omabslem  6640  infensuc  7035  infeq5i  7333  elom3  7345  omenps  7351  omensuc  7352  infdifsn  7353  cardlim  7601  r1om  7866  cfom  7886  ominf4  7934  alephom  8203  wunexALT  8359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511
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 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-tr 4115  df-eprel 4304  df-po 4313  df-so 4314  df-fr 4351  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656
  Copyright terms: Public domain W3C validator