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

Theorem 0lt1o 6707
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 2404 . 2  |-  (/)  =  (/)
2 el1o 6702 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 201 1  |-  (/)  e.  1o
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721   (/)c0 3588   1oc1o 6676
This theorem is referenced by:  dif20el  6708  oe1m  6747  oen0  6788  oeoa  6799  oeoe  6801  cantnf0  7586  isfin4-3  8151  fin1a2lem4  8239  1lt2pi  8738  indpi  8740  sadcp1  12922  vr1cl2  16546  fvcoe1  16560  vr1cl  16566  subrgvr1cl  16610  coe1mul2lem1  16615  coe1tm  16620  ply1coe  16639  xkofvcn  17669  evl1var  19905  pw2f1ocnv  26998  wepwsolem  27006
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-nul 4298
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-un 3285  df-nul 3589  df-sn 3780  df-suc 4547  df-1o 6683
  Copyright terms: Public domain W3C validator