Theorem 0lt1o 8429

Description: Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)

Assertion

Ref	Expression
0lt1o	⊢ ∅ ∈ 1o

Proof of Theorem 0lt1o

Step	Hyp	Ref	Expression
1		eqid 2739	. 2 ⊢ ∅ = ∅
2		el1o 8420	. 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅)
3	1, 2	mpbir 232	1 ⊢ ∅ ∈ 1o

Syntax hints:   = wceq 1547   ∈ wcel 2119  ∅c0 4261  1_oc1o 8388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-nul 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-un 3888  df-nul 4262  df-sn 4556  df-suc 6316  df-1o 8395

This theorem is referenced by:  dif20el  8430  oe1m  8470  oen0  8512  oeoa  8523  oeoe  8525  isfin4p1  10228  fin1a2lem4  10316  1lt2pi  10819  indpi  10821  sadcp1  16415  vr1cl2  22178  fvcoe1  22192  vr1cl  22202  subrgvr1cl  22248  coe1mul2lem1  22253  coe1tm  22259  ply1coe  22284  evl1var  22322  evls1var  22324  rhmply1vr1  22370  xkofvcn  23667  selvply1rhmlema  33702  selvply1rhmlemb  33703  selvply1rhmlem1  33704  selvply1rhmlem2  33705  selvply1rhmlem4  33707  fineqvnttrclse  35305  pw2f1ocnv  43482  wepwsolem  43487  onexoegt  43689  oaordnrex  43740  omnord1ex  43749  omcl3g  43779  tfsconcatb0  43789  indthinc  49952  indthincALT  49953  prsthinc  49954  setc1oid  49985  funcsetc1ocl  49986  funcsetc1o  49987  isinito2lem  49988  isinito4  50037  setc1onsubc  50092