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

Theorem 0lt1o 6715
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 2412 . 2  |-  (/)  =  (/)
2 el1o 6710 . 2  |-  ( (/)  e.  1o  <->  (/)  =  (/) )
31, 2mpbir 201 1  |-  (/)  e.  1o
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721   (/)c0 3596   1oc1o 6684
This theorem is referenced by:  dif20el  6716  oe1m  6755  oen0  6796  oeoa  6807  oeoe  6809  cantnf0  7594  isfin4-3  8159  fin1a2lem4  8247  1lt2pi  8746  indpi  8748  sadcp1  12930  vr1cl2  16554  fvcoe1  16568  vr1cl  16574  subrgvr1cl  16618  coe1mul2lem1  16623  coe1tm  16628  ply1coe  16647  xkofvcn  17677  evl1var  19913  pw2f1ocnv  27006  wepwsolem  27014
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-nul 4306
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 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-v 2926  df-dif 3291  df-un 3293  df-nul 3597  df-sn 3788  df-suc 4555  df-1o 6691
  Copyright terms: Public domain W3C validator