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

Theorem 0lt1o 7751
Description: Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)
Assertion
Ref Expression
0lt1o ∅ ∈ 1𝑜

Proof of Theorem 0lt1o
StepHypRef Expression
1 eqid 2758 . 2 ∅ = ∅
2 el1o 7746 . 2 (∅ ∈ 1𝑜 ↔ ∅ = ∅)
31, 2mpbir 221 1 ∅ ∈ 1𝑜
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  wcel 2137  c0 4056  1𝑜c1o 7720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-nul 4939
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340  df-dif 3716  df-un 3718  df-nul 4057  df-sn 4320  df-suc 5888  df-1o 7727
This theorem is referenced by:  dif20el  7752  oe1m  7792  oen0  7833  oeoa  7844  oeoe  7846  isfin4-3  9327  fin1a2lem4  9415  1lt2pi  9917  indpi  9919  sadcp1  15377  vr1cl2  19763  fvcoe1  19777  vr1cl  19787  subrgvr1cl  19832  coe1mul2lem1  19837  coe1tm  19843  ply1coe  19866  evl1var  19900  evls1var  19902  xkofvcn  21687  pw2f1ocnv  38104  wepwsolem  38112
  Copyright terms: Public domain W3C validator