Theorem 0lt1o 8414

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  ∅c0 4278  1_oc1o 8373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5239

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-un 3902  df-nul 4279  df-sn 4572  df-suc 6307  df-1o 8380

This theorem is referenced by:  dif20el  8415  oe1m  8455  oen0  8496  oeoa  8507  oeoe  8509  isfin4p1  10201  fin1a2lem4  10289  1lt2pi  10791  indpi  10793  sadcp1  16361  vr1cl2  22100  fvcoe1  22115  vr1cl  22125  subrgvr1cl  22171  coe1mul2lem1  22176  coe1tm  22182  ply1coe  22208  evl1var  22246  evls1var  22248  rhmply1vr1  22297  xkofvcn  23594  fineqvnttrclse  35136  pw2f1ocnv  43070  wepwsolem  43075  onexoegt  43277  oaordnrex  43328  omnord1ex  43337  omcl3g  43367  tfsconcatb0  43377  indthinc  49494  indthincALT  49495  prsthinc  49496  setc1oid  49527  funcsetc1ocl  49528  funcsetc1o  49529  isinito2lem  49530  isinito4  49579  setc1onsubc  49634