Theorem 0lt1o 8296

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  ∅c0 4253  1_oc1o 8260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-sn 4559  df-suc 6257  df-1o 8267

This theorem is referenced by:  dif20el  8297  oe1m  8338  oen0  8379  oeoa  8390  oeoe  8392  isfin4p1  10002  fin1a2lem4  10090  1lt2pi  10592  indpi  10594  sadcp1  16090  vr1cl2  21274  fvcoe1  21288  vr1cl  21298  subrgvr1cl  21343  coe1mul2lem1  21348  coe1tm  21354  ply1coe  21377  evl1var  21412  evls1var  21414  xkofvcn  22743  pw2f1ocnv  40775  wepwsolem  40783  indthinc  46221  indthincALT  46222  prsthinc  46223