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

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

Proof of Theorem 0lt1o
StepHypRef Expression
1 eqid 2733 . 2 ∅ = ∅
2 el1o 8445 . 2 (∅ ∈ 1o ↔ ∅ = ∅)
31, 2mpbir 230 1 ∅ ∈ 1o
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  c0 4286  1oc1o 8409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5267
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449  df-dif 3917  df-un 3919  df-nul 4287  df-sn 4591  df-suc 6327  df-1o 8416
This theorem is referenced by:  dif20el  8455  oe1m  8496  oen0  8537  oeoa  8548  oeoe  8550  isfin4p1  10259  fin1a2lem4  10347  1lt2pi  10849  indpi  10851  sadcp1  16343  vr1cl2  21587  fvcoe1  21601  vr1cl  21611  subrgvr1cl  21656  coe1mul2lem1  21661  coe1tm  21667  ply1coe  21690  evl1var  21725  evls1var  21727  xkofvcn  23058  pw2f1ocnv  41408  wepwsolem  41416  onexoegt  41625  oaordnrex  41677  omnord1ex  41686  omcl3g  41716  indthinc  47162  indthincALT  47163  prsthinc  47164
  Copyright terms: Public domain W3C validator