Theorem 0lt1o 8432

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∅c0 4274  1_oc1o 8391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-un 3895  df-nul 4275  df-sn 4569  df-suc 6323  df-1o 8398

This theorem is referenced by:  dif20el  8433  oe1m  8473  oen0  8515  oeoa  8526  oeoe  8528  isfin4p1  10228  fin1a2lem4  10316  1lt2pi  10819  indpi  10821  sadcp1  16415  vr1cl2  22166  fvcoe1  22181  vr1cl  22191  subrgvr1cl  22237  coe1mul2lem1  22242  coe1tm  22248  ply1coe  22273  evl1var  22311  evls1var  22313  rhmply1vr1  22362  xkofvcn  23659  fineqvnttrclse  35284  pw2f1ocnv  43483  wepwsolem  43488  onexoegt  43690  oaordnrex  43741  omnord1ex  43750  omcl3g  43780  tfsconcatb0  43790  indthinc  49949  indthincALT  49950  prsthinc  49951  setc1oid  49982  funcsetc1ocl  49983  funcsetc1o  49984  isinito2lem  49985  isinito4  50034  setc1onsubc  50089