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

Theorem 0ellim 6377
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 6373 . . . 4 ¬ Lim ∅
2 limeq 6326 . . . 4 (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
31, 2mtbiri 327 . . 3 (𝐴 = ∅ → ¬ Lim 𝐴)
43necon2ai 2972 . 2 (Lim 𝐴𝐴 ≠ ∅)
5 limord 6374 . . 3 (Lim 𝐴 → Ord 𝐴)
6 ord0eln0 6369 . . 3 (Ord 𝐴 → (∅ ∈ 𝐴𝐴 ≠ ∅))
75, 6syl 17 . 2 (Lim 𝐴 → (∅ ∈ 𝐴𝐴 ≠ ∅))
84, 7mpbird 257 1 (Lim 𝐴 → ∅ ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wcel 2107  wne 2942  c0 4281  Ord word 6313  Lim wlim 6315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-tr 5222  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-ord 6317  df-lim 6319
This theorem is referenced by:  limuni3  7779  peano1  7816  peano1OLD  7817  oe1m  8460  oalimcl  8475  oaass  8476  oarec  8477  omlimcl  8493  odi  8494  oen0  8501  oewordri  8507  oelim2  8510  oeoalem  8511  oeoelem  8513  limensuci  9031  rankxplim2  9750  rankxplim3  9751  r1limwun  10606  omlimcl2  41453
  Copyright terms: Public domain W3C validator