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

Theorem 0ellim 6091
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 6087 . . . 4 ¬ Lim ∅
2 limeq 6041 . . . 4 (𝐴 = ∅ → (Lim 𝐴 ↔ Lim ∅))
31, 2mtbiri 319 . . 3 (𝐴 = ∅ → ¬ Lim 𝐴)
43necon2ai 2996 . 2 (Lim 𝐴𝐴 ≠ ∅)
5 limord 6088 . . 3 (Lim 𝐴 → Ord 𝐴)
6 ord0eln0 6083 . . 3 (Ord 𝐴 → (∅ ∈ 𝐴𝐴 ≠ ∅))
75, 6syl 17 . 2 (Lim 𝐴 → (∅ ∈ 𝐴𝐴 ≠ ∅))
84, 7mpbird 249 1 (Lim 𝐴 → ∅ ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1507  wcel 2050  wne 2967  c0 4178  Ord word 6028  Lim wlim 6030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3682  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-tr 5031  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-ord 6032  df-lim 6034
This theorem is referenced by:  limuni3  7383  peano1  7416  oe1m  7972  oalimcl  7987  oaass  7988  oarec  7989  omlimcl  8005  odi  8006  oen0  8013  oewordri  8019  oelim2  8022  oeoalem  8023  oeoelem  8025  limensuci  8489  rankxplim2  9103  rankxplim3  9104  r1limwun  9956
  Copyright terms: Public domain W3C validator