Theorem 0lt1o 8541

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

Syntax hints:   = wceq 1537   ∈ wcel 2106  ∅c0 4339  1_oc1o 8498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-un 3968  df-nul 4340  df-sn 4632  df-suc 6392  df-1o 8505

This theorem is referenced by:  dif20el  8542  oe1m  8582  oen0  8623  oeoa  8634  oeoe  8636  isfin4p1  10353  fin1a2lem4  10441  1lt2pi  10943  indpi  10945  sadcp1  16489  vr1cl2  22210  fvcoe1  22225  vr1cl  22235  subrgvr1cl  22281  coe1mul2lem1  22286  coe1tm  22292  ply1coe  22318  evl1var  22356  evls1var  22358  rhmply1vr1  22407  xkofvcn  23708  pw2f1ocnv  43026  wepwsolem  43031  onexoegt  43233  oaordnrex  43285  omnord1ex  43294  omcl3g  43324  tfsconcatb0  43334  indthinc  48853  indthincALT  48854  prsthinc  48855