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

Theorem 0ellim 5440
Description: A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.)
Assertion
Ref Expression
0ellim  |-  ( Lim 
A  ->  (/)  e.  A
)

Proof of Theorem 0ellim
StepHypRef Expression
1 nlim0 5436 . . . 4  |-  -.  Lim  (/)
2 limeq 5390 . . . 4  |-  ( A  =  (/)  ->  ( Lim 
A  <->  Lim  (/) ) )
31, 2mtbiri 304 . . 3  |-  ( A  =  (/)  ->  -.  Lim  A )
43necon2ai 2624 . 2  |-  ( Lim 
A  ->  A  =/=  (/) )
5 limord 5437 . . 3  |-  ( Lim 
A  ->  Ord  A )
6 ord0eln0 5432 . . 3  |-  ( Ord 
A  ->  ( (/)  e.  A  <->  A  =/=  (/) ) )
75, 6syl 17 . 2  |-  ( Lim 
A  ->  ( (/)  e.  A  <->  A  =/=  (/) ) )
84, 7mpbird 235 1  |-  ( Lim 
A  ->  (/)  e.  A
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1872    =/= wne 2593   (/)c0 3697   Ord word 5377   Lim wlim 5379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-sep 4482  ax-nul 4491  ax-pr 4596
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-rab 2717  df-v 3018  df-sbc 3236  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-op 3941  df-uni 4156  df-br 4360  df-opab 4419  df-tr 4455  df-eprel 4700  df-po 4710  df-so 4711  df-fr 4748  df-we 4750  df-ord 5381  df-lim 5383
This theorem is referenced by:  limuni3  6630  peano1  6663  oe1m  7194  oalimcl  7209  oaass  7210  oarec  7211  omlimcl  7227  odi  7228  oen0  7235  oewordri  7241  oelim2  7244  oeoalem  7245  oeoelem  7247  limensuci  7694  rankxplim2  8296  rankxplim3  8297  r1limwun  9105
  Copyright terms: Public domain W3C validator