Theorem 0lt1o 8123

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 2821	. 2 ⊢ ∅ = ∅
2		el1o 8118	. 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅)
3	1, 2	mpbir 233	1 ⊢ ∅ ∈ 1o

Syntax hints:   = wceq 1533   ∈ wcel 2110  ∅c0 4290  1_oc1o 8089

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-nul 5202

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3938  df-un 3940  df-nul 4291  df-sn 4561  df-suc 6191  df-1o 8096

This theorem is referenced by:  dif20el  8124  oe1m  8165  oen0  8206  oeoa  8217  oeoe  8219  isfin4p1  9731  fin1a2lem4  9819  1lt2pi  10321  indpi  10323  sadcp1  15798  vr1cl2  20355  fvcoe1  20369  vr1cl  20379  subrgvr1cl  20424  coe1mul2lem1  20429  coe1tm  20435  ply1coe  20458  evl1var  20493  evls1var  20495  xkofvcn  22286  pw2f1ocnv  39627  wepwsolem  39635