Theorem 0lt1o 8445

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 2729	. 2 ⊢ ∅ = ∅
2		el1o 8436	. 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅)
3	1, 2	mpbir 231	1 ⊢ ∅ ∈ 1o

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∅c0 4292  1_oc1o 8404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-un 3916  df-nul 4293  df-sn 4586  df-suc 6326  df-1o 8411

This theorem is referenced by:  dif20el  8446  oe1m  8486  oen0  8527  oeoa  8538  oeoe  8540  isfin4p1  10244  fin1a2lem4  10332  1lt2pi  10834  indpi  10836  sadcp1  16401  vr1cl2  22053  fvcoe1  22068  vr1cl  22078  subrgvr1cl  22124  coe1mul2lem1  22129  coe1tm  22135  ply1coe  22161  evl1var  22199  evls1var  22201  rhmply1vr1  22250  xkofvcn  23547  pw2f1ocnv  42999  wepwsolem  43004  onexoegt  43206  oaordnrex  43257  omnord1ex  43266  omcl3g  43296  tfsconcatb0  43306  indthinc  49424  indthincALT  49425  prsthinc  49426  setc1oid  49457  funcsetc1ocl  49458  funcsetc1o  49459  isinito2lem  49460  isinito4  49509  setc1onsubc  49564