Theorem 0lt1o 8534

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 2726	. 2 ⊢ ∅ = ∅
2		el1o 8525	. 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅)
3	1, 2	mpbir 230	1 ⊢ ∅ ∈ 1o

Syntax hints:   = wceq 1534   ∈ wcel 2099  ∅c0 4325  1_oc1o 8489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-nul 5311

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3950  df-un 3952  df-nul 4326  df-sn 4634  df-suc 6382  df-1o 8496

This theorem is referenced by:  dif20el  8535  oe1m  8575  oen0  8616  oeoa  8627  oeoe  8629  isfin4p1  10358  fin1a2lem4  10446  1lt2pi  10948  indpi  10950  sadcp1  16455  vr1cl2  22182  fvcoe1  22197  vr1cl  22207  subrgvr1cl  22253  coe1mul2lem1  22258  coe1tm  22264  ply1coe  22289  evl1var  22327  evls1var  22329  rhmply1vr1  22378  xkofvcn  23679  pw2f1ocnv  42695  wepwsolem  42703  onexoegt  42909  oaordnrex  42961  omnord1ex  42970  omcl3g  43000  tfsconcatb0  43010  indthinc  48373  indthincALT  48374  prsthinc  48375