Theorem 0lt1o 8429

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∅c0 4286  1_oc1o 8388

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 5248

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 3440  df-dif 3908  df-un 3910  df-nul 4287  df-sn 4580  df-suc 6317  df-1o 8395

This theorem is referenced by:  dif20el  8430  oe1m  8470  oen0  8511  oeoa  8522  oeoe  8524  isfin4p1  10228  fin1a2lem4  10316  1lt2pi  10818  indpi  10820  sadcp1  16385  vr1cl2  22094  fvcoe1  22109  vr1cl  22119  subrgvr1cl  22165  coe1mul2lem1  22170  coe1tm  22176  ply1coe  22202  evl1var  22240  evls1var  22242  rhmply1vr1  22291  xkofvcn  23588  pw2f1ocnv  43030  wepwsolem  43035  onexoegt  43237  oaordnrex  43288  omnord1ex  43297  omcl3g  43327  tfsconcatb0  43337  indthinc  49467  indthincALT  49468  prsthinc  49469  setc1oid  49500  funcsetc1ocl  49501  funcsetc1o  49502  isinito2lem  49503  isinito4  49552  setc1onsubc  49607