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

Theorem 0lt1o 8128
 Description: Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)
Assertion
Ref Expression
0lt1o ∅ ∈ 1o

Proof of Theorem 0lt1o
StepHypRef Expression
1 eqid 2821 . 2 ∅ = ∅
2 el1o 8123 . 2 (∅ ∈ 1o ↔ ∅ = ∅)
31, 2mpbir 233 1 ∅ ∈ 1o
 Colors of variables: wff setvar class Syntax hints:   = wceq 1533   ∈ wcel 2110  ∅c0 4290  1oc1o 8094 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-nul 5209 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3938  df-un 3940  df-nul 4291  df-sn 4567  df-suc 6196  df-1o 8101 This theorem is referenced by:  dif20el  8129  oe1m  8170  oen0  8211  oeoa  8222  oeoe  8224  isfin4p1  9736  fin1a2lem4  9824  1lt2pi  10326  indpi  10328  sadcp1  15803  vr1cl2  20360  fvcoe1  20374  vr1cl  20384  subrgvr1cl  20429  coe1mul2lem1  20434  coe1tm  20440  ply1coe  20463  evl1var  20498  evls1var  20500  xkofvcn  22291  pw2f1ocnv  39634  wepwsolem  39642
 Copyright terms: Public domain W3C validator