Theorem 0lt1o 7751

Description: Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)

Assertion

Ref	Expression
0lt1o	⊢ ∅ ∈ 1𝑜

Proof of Theorem 0lt1o

Step	Hyp	Ref	Expression
1		eqid 2758	. 2 ⊢ ∅ = ∅
2		el1o 7746	. 2 ⊢ (∅ ∈ 1𝑜 ↔ ∅ = ∅)
3	1, 2	mpbir 221	1 ⊢ ∅ ∈ 1𝑜

Syntax hints:   = wceq 1630   ∈ wcel 2137  ∅c0 4056  1_𝑜c1o 7720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-nul 4939

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340  df-dif 3716  df-un 3718  df-nul 4057  df-sn 4320  df-suc 5888  df-1o 7727

This theorem is referenced by:  dif20el  7752  oe1m  7792  oen0  7833  oeoa  7844  oeoe  7846  isfin4-3  9327  fin1a2lem4  9415  1lt2pi  9917  indpi  9919  sadcp1  15377  vr1cl2  19763  fvcoe1  19777  vr1cl  19787  subrgvr1cl  19832  coe1mul2lem1  19837  coe1tm  19843  ply1coe  19866  evl1var  19900  evls1var  19902  xkofvcn  21687  pw2f1ocnv  38104  wepwsolem  38112