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

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

Proof of Theorem 0lt1o
StepHypRef Expression
1 eqid 2283 . 2  |-  (/)  =  (/)
2 el1o 6498 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 200 1  |-  (/)  e.  1o
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684   (/)c0 3455   1oc1o 6472
This theorem is referenced by:  dif20el  6504  oe1m  6543  oen0  6584  oeoa  6595  oeoe  6597  cantnf0  7376  isfin4-3  7941  fin1a2lem4  8029  1lt2pi  8529  indpi  8531  sadcp1  12646  vr1cl2  16272  fvcoe1  16288  vr1cl  16294  subrgvr1cl  16339  coe1mul2lem1  16344  coe1tm  16349  ply1coe  16368  xkofvcn  17378  evl1var  19415  empklst  26009  pw2f1ocnv  27130  wepwsolem  27138
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-un 3157  df-nul 3456  df-sn 3646  df-suc 4398  df-1o 6479
  Copyright terms: Public domain W3C validator