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

Theorem 0lt1o 6944
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 2443 . 2  |-  (/)  =  (/)
2 el1o 6939 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 209 1  |-  (/)  e.  1o
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756   (/)c0 3637   1oc1o 6913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-v 2974  df-dif 3331  df-un 3333  df-nul 3638  df-sn 3878  df-suc 4725  df-1o 6920
This theorem is referenced by:  dif20el  6945  oe1m  6984  oen0  7025  oeoa  7036  oeoe  7038  isfin4-3  8484  fin1a2lem4  8572  1lt2pi  9074  indpi  9076  sadcp1  13651  vr1cl2  17649  fvcoe1  17663  vr1cl  17671  subrgvr1cl  17716  coe1mul2lem1  17721  coe1tm  17726  ply1coe  17746  ply1coeOLD  17747  evl1var  17770  evls1var  17772  xkofvcn  19257  pw2f1ocnv  29386  wepwsolem  29394
  Copyright terms: Public domain W3C validator