Theorem 0lt1o 8455

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  ∅c0 4287  1_oc1o 8410

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-nul 5268

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916  df-un 3918  df-nul 4288  df-sn 4592  df-suc 6328  df-1o 8417

This theorem is referenced by:  dif20el  8456  oe1m  8497  oen0  8538  oeoa  8549  oeoe  8551  isfin4p1  10260  fin1a2lem4  10348  1lt2pi  10850  indpi  10852  sadcp1  16346  vr1cl2  21601  fvcoe1  21615  vr1cl  21625  subrgvr1cl  21670  coe1mul2lem1  21675  coe1tm  21681  ply1coe  21704  evl1var  21739  evls1var  21741  xkofvcn  23072  pw2f1ocnv  41419  wepwsolem  41427  onexoegt  41636  oaordnrex  41688  omnord1ex  41697  omcl3g  41727  tfsconcatb0  41737  indthinc  47192  indthincALT  47193  prsthinc  47194