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

Theorem limom 6714
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 6708 . 2  |-  Ord  om
2 ordeleqon 6623 . . 3  |-  ( Ord 
om 
<->  ( om  e.  On  \/  om  =  On ) )
3 ordirr 4905 . . . . . . 7  |-  ( Ord 
om  ->  -.  om  e.  om )
41, 3ax-mp 5 . . . . . 6  |-  -.  om  e.  om
5 elom 6702 . . . . . . 7  |-  ( om  e.  om  <->  ( om  e.  On  /\  A. x
( Lim  x  ->  om  e.  x ) ) )
65baib 903 . . . . . 6  |-  ( om  e.  On  ->  ( om  e.  om  <->  A. x
( Lim  x  ->  om  e.  x ) ) )
74, 6mtbii 302 . . . . 5  |-  ( om  e.  On  ->  -.  A. x ( Lim  x  ->  om  e.  x ) )
8 limomss 6704 . . . . . . . . . . 11  |-  ( Lim  x  ->  om  C_  x
)
9 limord 4946 . . . . . . . . . . . 12  |-  ( Lim  x  ->  Ord  x )
10 ordsseleq 4916 . . . . . . . . . . . 12  |-  ( ( Ord  om  /\  Ord  x )  ->  ( om  C_  x  <->  ( om  e.  x  \/  om  =  x ) ) )
111, 9, 10sylancr 663 . . . . . . . . . . 11  |-  ( Lim  x  ->  ( om  C_  x  <->  ( om  e.  x  \/  om  =  x ) ) )
128, 11mpbid 210 . . . . . . . . . 10  |-  ( Lim  x  ->  ( om  e.  x  \/  om  =  x ) )
1312ord 377 . . . . . . . . 9  |-  ( Lim  x  ->  ( -.  om  e.  x  ->  om  =  x ) )
14 limeq 4899 . . . . . . . . . 10  |-  ( om  =  x  ->  ( Lim  om  <->  Lim  x ) )
1514biimprcd 225 . . . . . . . . 9  |-  ( Lim  x  ->  ( om  =  x  ->  Lim  om ) )
1613, 15syld 44 . . . . . . . 8  |-  ( Lim  x  ->  ( -.  om  e.  x  ->  Lim  om ) )
1716con1d 124 . . . . . . 7  |-  ( Lim  x  ->  ( -.  Lim  om  ->  om  e.  x ) )
1817com12 31 . . . . . 6  |-  ( -. 
Lim  om  ->  ( Lim  x  ->  om  e.  x ) )
1918alrimiv 1720 . . . . 5  |-  ( -. 
Lim  om  ->  A. x
( Lim  x  ->  om  e.  x ) )
207, 19nsyl2 127 . . . 4  |-  ( om  e.  On  ->  Lim  om )
21 limon 6670 . . . . 5  |-  Lim  On
22 limeq 4899 . . . . 5  |-  ( om  =  On  ->  ( Lim  om  <->  Lim  On ) )
2321, 22mpbiri 233 . . . 4  |-  ( om  =  On  ->  Lim  om )
2420, 23jaoi 379 . . 3  |-  ( ( om  e.  On  \/  om  =  On )  ->  Lim  om )
252, 24sylbi 195 . 2  |-  ( Ord 
om  ->  Lim  om )
261, 25ax-mp 5 1  |-  Lim  om
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368   A.wal 1393    = wceq 1395    e. wcel 1819    C_ wss 3471   Ord word 4886   Oncon0 4887   Lim wlim 4888   omcom 6699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-tr 4551  df-eprel 4800  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-om 6700
This theorem is referenced by:  peano2b  6715  ssnlim  6717  peano1  6718  onesuc  7198  oaabslem  7310  oaabs2  7312  omabslem  7313  infensuc  7714  infeq5i  8070  elom3  8082  omenps  8088  omensuc  8089  infdifsn  8090  cardlim  8370  r1om  8641  cfom  8661  ominf4  8709  alephom  8977  wunex3  9136
  Copyright terms: Public domain W3C validator