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

Theorem 0lt1o 6940
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 2441 . 2  |-  (/)  =  (/)
2 el1o 6935 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 209 1  |-  (/)  e.  1o
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364    e. wcel 1761   (/)c0 3634   1oc1o 6909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-nul 4418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-v 2972  df-dif 3328  df-un 3330  df-nul 3635  df-sn 3875  df-suc 4721  df-1o 6916
This theorem is referenced by:  dif20el  6941  oe1m  6980  oen0  7021  oeoa  7032  oeoe  7034  isfin4-3  8480  fin1a2lem4  8568  1lt2pi  9070  indpi  9072  sadcp1  13647  vr1cl2  17625  fvcoe1  17639  vr1cl  17647  subrgvr1cl  17691  coe1mul2lem1  17696  coe1tm  17701  ply1coe  17720  evl1var  17739  evls1var  17741  xkofvcn  19216  pw2f1ocnv  29311  wepwsolem  29319
  Copyright terms: Public domain W3C validator