Theorem 0lt1o 8441

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∅c0 4287  1_oc1o 8400

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 5253

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 3444  df-dif 3906  df-un 3908  df-nul 4288  df-sn 4583  df-suc 6331  df-1o 8407

This theorem is referenced by:  dif20el  8442  oe1m  8482  oen0  8524  oeoa  8535  oeoe  8537  isfin4p1  10237  fin1a2lem4  10325  1lt2pi  10828  indpi  10830  sadcp1  16394  vr1cl2  22145  fvcoe1  22160  vr1cl  22170  subrgvr1cl  22216  coe1mul2lem1  22221  coe1tm  22227  ply1coe  22254  evl1var  22292  evls1var  22294  rhmply1vr1  22343  xkofvcn  23640  fineqvnttrclse  35302  pw2f1ocnv  43394  wepwsolem  43399  onexoegt  43601  oaordnrex  43652  omnord1ex  43661  omcl3g  43691  tfsconcatb0  43701  indthinc  49821  indthincALT  49822  prsthinc  49823  setc1oid  49854  funcsetc1ocl  49855  funcsetc1o  49856  isinito2lem  49857  isinito4  49906  setc1onsubc  49961