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

Theorem 0lt1o 6587
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 2358 . 2  |-  (/)  =  (/)
2 el1o 6582 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 200 1  |-  (/)  e.  1o
Colors of variables: wff set class
Syntax hints:    = wceq 1642    e. wcel 1710   (/)c0 3531   1oc1o 6556
This theorem is referenced by:  dif20el  6588  oe1m  6627  oen0  6668  oeoa  6679  oeoe  6681  cantnf0  7463  isfin4-3  8028  fin1a2lem4  8116  1lt2pi  8616  indpi  8618  sadcp1  12737  vr1cl2  16365  fvcoe1  16381  vr1cl  16387  subrgvr1cl  16432  coe1mul2lem1  16437  coe1tm  16442  ply1coe  16461  xkofvcn  17478  evl1var  19513  pw2f1ocnv  26453  wepwsolem  26461
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-nul 4228
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-v 2866  df-dif 3231  df-un 3233  df-nul 3532  df-sn 3722  df-suc 4477  df-1o 6563
  Copyright terms: Public domain W3C validator