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

Theorem 0ellim 6439
Description: A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.)
Assertion
Ref Expression
0ellim (Lim 𝐴 → ∅ ∈ 𝐴)

Proof of Theorem 0ellim
StepHypRef Expression
1 nlim0 6435 . . . 4 ¬ Lim ∅
2 limeq 6388 . . . 4 (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
31, 2mtbiri 326 . . 3 (𝐴 = ∅ → ¬ Lim 𝐴)
43necon2ai 2960 . 2 (Lim 𝐴𝐴 ≠ ∅)
5 limord 6436 . . 3 (Lim 𝐴 → Ord 𝐴)
6 ord0eln0 6431 . . 3 (Ord 𝐴 → (∅ ∈ 𝐴𝐴 ≠ ∅))
75, 6syl 17 . 2 (Lim 𝐴 → (∅ ∈ 𝐴𝐴 ≠ ∅))
84, 7mpbird 256 1 (Lim 𝐴 → ∅ ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1534  wcel 2099  wne 2930  c0 4325  Ord word 6375  Lim wlim 6377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-tr 5271  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-ord 6379  df-lim 6381
This theorem is referenced by:  limuni3  7862  peano1  7900  peano1OLD  7901  oe1m  8575  oalimcl  8590  oaass  8591  oarec  8592  omlimcl  8608  odi  8609  oen0  8616  oewordri  8622  oelim2  8625  oeoalem  8626  oeoelem  8628  limensuci  9191  rankxplim2  9923  rankxplim3  9924  r1limwun  10779  constr01  33600  omlimcl2  42907  oe0suclim  42943
  Copyright terms: Public domain W3C validator