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

Theorem 0lt1o 7214
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 2429 . 2  |-  (/)  =  (/)
2 el1o 7209 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 212 1  |-  (/)  e.  1o
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1870   (/)c0 3767   1oc1o 7183
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-v 3089  df-dif 3445  df-un 3447  df-nul 3768  df-sn 4003  df-suc 5448  df-1o 7190
This theorem is referenced by:  dif20el  7215  oe1m  7254  oen0  7295  oeoa  7306  oeoe  7308  isfin4-3  8743  fin1a2lem4  8831  1lt2pi  9329  indpi  9331  sadcp1  14403  vr1cl2  18721  fvcoe1  18735  vr1cl  18745  subrgvr1cl  18790  coe1mul2lem1  18795  coe1tm  18801  ply1coe  18824  ply1coeOLD  18825  evl1var  18859  evls1var  18861  xkofvcn  20630  pw2f1ocnv  35598  wepwsolem  35606
  Copyright terms: Public domain W3C validator