Theorem 0lt1o 8505

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ∅c0 4279  1_oc1o 8462

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-un 3904  df-nul 4280  df-sn 4585  df-suc 6367  df-1o 8469

This theorem is used by:  dif20el  8506  oe1m  8546  oen0  8588  oeoa  8599  oeoe  8601  isfin4p1  10386  fin1a2lem4  10474  1lt2pi  10983  indpi  10985  sadcp1  16618  vr1cl2  22504  fvcoe1  22518  vr1cl  22528  subrgvr1cl  22574  coe1mul2lem1  22579  coe1tm  22585  ply1coe  22609  evl1var  22647  evls1var  22649  rhmply1vr1  22695  xkofvcn  23996  selvply1rhmlema  34143  selvply1rhmlemb  34144  selvply1rhmlem1  34145  selvply1rhmlem2  34146  selvply1rhmlem4  34148  fineqvnttrclse  35775  pw2f1ocnv  44023  wepwsolem  44028  onexoegt  44230  oaordnrex  44281  omnord1ex  44290  omcl3g  44320  tfsconcatb0  44330  indthinc  50539  indthincALT  50540  prsthinc  50541  setc1oid  50572  funcsetc1ocl  50573  funcsetc1o  50574  isinito2lem  50575  isinito4  50624  setc1onsubc  50679