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

Theorem 0lt1o 6777
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 2442 . 2  |-  (/)  =  (/)
2 el1o 6772 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 202 1  |-  (/)  e.  1o
Colors of variables: wff set class
Syntax hints:    = wceq 1653    e. wcel 1727   (/)c0 3613   1oc1o 6746
This theorem is referenced by:  dif20el  6778  oe1m  6817  oen0  6858  oeoa  6869  oeoe  6871  cantnf0  7659  isfin4-3  8226  fin1a2lem4  8314  1lt2pi  8813  indpi  8815  sadcp1  12998  vr1cl2  16622  fvcoe1  16636  vr1cl  16642  subrgvr1cl  16686  coe1mul2lem1  16691  coe1tm  16696  ply1coe  16715  xkofvcn  17747  evl1var  19983  pw2f1ocnv  27146  wepwsolem  27154
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-nul 4363
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-v 2964  df-dif 3309  df-un 3311  df-nul 3614  df-sn 3844  df-suc 4616  df-1o 6753
  Copyright terms: Public domain W3C validator