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

Theorem 0lt1o 6519
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 2296 . 2  |-  (/)  =  (/)
2 el1o 6514 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 200 1  |-  (/)  e.  1o
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696   (/)c0 3468   1oc1o 6488
This theorem is referenced by:  dif20el  6520  oe1m  6559  oen0  6600  oeoa  6611  oeoe  6613  cantnf0  7392  isfin4-3  7957  fin1a2lem4  8045  1lt2pi  8545  indpi  8547  sadcp1  12662  vr1cl2  16288  fvcoe1  16304  vr1cl  16310  subrgvr1cl  16355  coe1mul2lem1  16360  coe1tm  16365  ply1coe  16384  xkofvcn  17394  evl1var  19431  empklst  26112  pw2f1ocnv  27233  wepwsolem  27241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-nul 4165
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-un 3170  df-nul 3469  df-sn 3659  df-suc 4414  df-1o 6495
  Copyright terms: Public domain W3C validator