Theorem 0lt1o 8439

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∅c0 4273  1_oc1o 8398

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274  df-sn 4568  df-suc 6329  df-1o 8405

This theorem is referenced by:  dif20el  8440  oe1m  8480  oen0  8522  oeoa  8533  oeoe  8535  isfin4p1  10237  fin1a2lem4  10325  1lt2pi  10828  indpi  10830  sadcp1  16424  vr1cl2  22156  fvcoe1  22171  vr1cl  22181  subrgvr1cl  22227  coe1mul2lem1  22232  coe1tm  22238  ply1coe  22263  evl1var  22301  evls1var  22303  rhmply1vr1  22352  xkofvcn  23649  fineqvnttrclse  35268  pw2f1ocnv  43465  wepwsolem  43470  onexoegt  43672  oaordnrex  43723  omnord1ex  43732  omcl3g  43762  tfsconcatb0  43772  indthinc  49937  indthincALT  49938  prsthinc  49939  setc1oid  49970  funcsetc1ocl  49971  funcsetc1o  49972  isinito2lem  49973  isinito4  50022  setc1onsubc  50077