Theorem 0lt1o 8112

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 2798	. 2 ⊢ ∅ = ∅
2		el1o 8107	. 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅)
3	1, 2	mpbir 234	1 ⊢ ∅ ∈ 1o

Syntax hints:   = wceq 1538   ∈ wcel 2111  ∅c0 4243  1_oc1o 8078

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-un 3886  df-nul 4244  df-sn 4526  df-suc 6165  df-1o 8085

This theorem is referenced by:  dif20el  8113  oe1m  8154  oen0  8195  oeoa  8206  oeoe  8208  isfin4p1  9726  fin1a2lem4  9814  1lt2pi  10316  indpi  10318  sadcp1  15794  vr1cl2  20822  fvcoe1  20836  vr1cl  20846  subrgvr1cl  20891  coe1mul2lem1  20896  coe1tm  20902  ply1coe  20925  evl1var  20960  evls1var  20962  xkofvcn  22289  pw2f1ocnv  39978  wepwsolem  39986