Theorem 0lt1o 8560

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 2740	. 2 ⊢ ∅ = ∅
2		el1o 8551	. 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅)
3	1, 2	mpbir 231	1 ⊢ ∅ ∈ 1o

Syntax hints:   = wceq 1537   ∈ wcel 2108  ∅c0 4352  1_oc1o 8515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353  df-sn 4649  df-suc 6401  df-1o 8522

This theorem is referenced by:  dif20el  8561  oe1m  8601  oen0  8642  oeoa  8653  oeoe  8655  isfin4p1  10384  fin1a2lem4  10472  1lt2pi  10974  indpi  10976  sadcp1  16501  vr1cl2  22215  fvcoe1  22230  vr1cl  22240  subrgvr1cl  22286  coe1mul2lem1  22291  coe1tm  22297  ply1coe  22323  evl1var  22361  evls1var  22363  rhmply1vr1  22412  xkofvcn  23713  pw2f1ocnv  42994  wepwsolem  42999  onexoegt  43205  oaordnrex  43257  omnord1ex  43266  omcl3g  43296  tfsconcatb0  43306  indthinc  48719  indthincALT  48720  prsthinc  48721