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

Theorem 0lt1o 6686
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 2389 . 2  |-  (/)  =  (/)
2 el1o 6681 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 201 1  |-  (/)  e.  1o
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1717   (/)c0 3573   1oc1o 6655
This theorem is referenced by:  dif20el  6687  oe1m  6726  oen0  6767  oeoa  6778  oeoe  6780  cantnf0  7565  isfin4-3  8130  fin1a2lem4  8218  1lt2pi  8717  indpi  8719  sadcp1  12896  vr1cl2  16520  fvcoe1  16534  vr1cl  16540  subrgvr1cl  16584  coe1mul2lem1  16589  coe1tm  16594  ply1coe  16613  xkofvcn  17639  evl1var  19821  pw2f1ocnv  26801  wepwsolem  26809
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-nul 4281
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 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-v 2903  df-dif 3268  df-un 3270  df-nul 3574  df-sn 3765  df-suc 4530  df-1o 6662
  Copyright terms: Public domain W3C validator