Theorem 0lt1o 8334

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

Syntax hints:   = wceq 1539   ∈ wcel 2106  ∅c0 4256  1_oc1o 8290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-sn 4562  df-suc 6272  df-1o 8297

This theorem is referenced by:  dif20el  8335  oe1m  8376  oen0  8417  oeoa  8428  oeoe  8430  isfin4p1  10071  fin1a2lem4  10159  1lt2pi  10661  indpi  10663  sadcp1  16162  vr1cl2  21364  fvcoe1  21378  vr1cl  21388  subrgvr1cl  21433  coe1mul2lem1  21438  coe1tm  21444  ply1coe  21467  evl1var  21502  evls1var  21504  xkofvcn  22835  pw2f1ocnv  40859  wepwsolem  40867  indthinc  46333  indthincALT  46334  prsthinc  46335