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

Theorem 0lt1o 7154
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 2467 . 2  |-  (/)  =  (/)
2 el1o 7149 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 209 1  |-  (/)  e.  1o
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    e. wcel 1767   (/)c0 3785   1oc1o 7123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-un 3481  df-nul 3786  df-sn 4028  df-suc 4884  df-1o 7130
This theorem is referenced by:  dif20el  7155  oe1m  7194  oen0  7235  oeoa  7246  oeoe  7248  isfin4-3  8695  fin1a2lem4  8783  1lt2pi  9283  indpi  9285  sadcp1  13964  vr1cl2  18031  fvcoe1  18045  vr1cl  18057  subrgvr1cl  18102  coe1mul2lem1  18107  coe1tm  18113  ply1coe  18136  ply1coeOLD  18137  evl1var  18171  evls1var  18173  xkofvcn  19948  pw2f1ocnv  30611  wepwsolem  30619
  Copyright terms: Public domain W3C validator