Theorem 0lt1o 8131

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  ∅c0 4293  1_oc1o 8097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-nul 5212

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-un 3943  df-nul 4294  df-sn 4570  df-suc 6199  df-1o 8104

This theorem is referenced by:  dif20el  8132  oe1m  8173  oen0  8214  oeoa  8225  oeoe  8227  isfin4p1  9739  fin1a2lem4  9827  1lt2pi  10329  indpi  10331  sadcp1  15806  vr1cl2  20363  fvcoe1  20377  vr1cl  20387  subrgvr1cl  20432  coe1mul2lem1  20437  coe1tm  20443  ply1coe  20466  evl1var  20501  evls1var  20503  xkofvcn  22294  pw2f1ocnv  39641  wepwsolem  39649