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

Theorem ord0eln0 6430
Description: A nonempty ordinal contains the empty set. Lemma 1.10 of [Schloeder] p. 2. (Contributed by NM, 25-Nov-1995.)
Assertion
Ref Expression
ord0eln0 (Ord 𝐴 → (∅ ∈ 𝐴𝐴 ≠ ∅))

Proof of Theorem ord0eln0
StepHypRef Expression
1 ne0i 4336 . 2 (∅ ∈ 𝐴𝐴 ≠ ∅)
2 ord0 6428 . . . 4 Ord ∅
3 noel 4332 . . . . 5 ¬ 𝐴 ∈ ∅
4 ordtri2 6410 . . . . . 6 ((Ord 𝐴 ∧ Ord ∅) → (𝐴 ∈ ∅ ↔ ¬ (𝐴 = ∅ ∨ ∅ ∈ 𝐴)))
54con2bid 353 . . . . 5 ((Ord 𝐴 ∧ Ord ∅) → ((𝐴 = ∅ ∨ ∅ ∈ 𝐴) ↔ ¬ 𝐴 ∈ ∅))
63, 5mpbiri 257 . . . 4 ((Ord 𝐴 ∧ Ord ∅) → (𝐴 = ∅ ∨ ∅ ∈ 𝐴))
72, 6mpan2 689 . . 3 (Ord 𝐴 → (𝐴 = ∅ ∨ ∅ ∈ 𝐴))
8 neor 3023 . . 3 ((𝐴 = ∅ ∨ ∅ ∈ 𝐴) ↔ (𝐴 ≠ ∅ → ∅ ∈ 𝐴))
97, 8sylib 217 . 2 (Ord 𝐴 → (𝐴 ≠ ∅ → ∅ ∈ 𝐴))
101, 9impbid2 225 1 (Ord 𝐴 → (∅ ∈ 𝐴𝐴 ≠ ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845   = wceq 1533  wcel 2098  wne 2929  c0 4324  Ord word 6374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-tr 5270  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-ord 6378
This theorem is referenced by:  on0eln0  6431  dflim2  6432  0ellim  6438  0elsuc  7843  ordge1n0  8523  omwordi  8600  omass  8609  nnmord  8661  nnmwordi  8664  wemapwe  9736  elni2  10916  cuteq1  27855  bnj529  34554  ordeldif1o  42875  ordne0gt0  42876  dflim7  42888
  Copyright terms: Public domain W3C validator