Theorem 0lt1o 8491

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

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

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 2732  ax-nul 5263

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-un 3904  df-nul 4280  df-sn 4585  df-suc 6363  df-1o 8455

This theorem is used by:  dif20el  8492  oe1m  8532  oen0  8574  oeoa  8585  oeoe  8587  isfin4p1  10317  fin1a2lem4  10405  1lt2pi  10914  indpi  10916  sadcp1  16545  vr1cl2  22418  fvcoe1  22432  vr1cl  22442  subrgvr1cl  22488  coe1mul2lem1  22493  coe1tm  22499  ply1coe  22523  evl1var  22561  evls1var  22563  rhmply1vr1  22609  xkofvcn  23910  selvply1rhmlema  34028  selvply1rhmlemb  34029  selvply1rhmlem1  34030  selvply1rhmlem2  34031  selvply1rhmlem4  34033  fineqvnttrclse  35650  pw2f1ocnv  43878  wepwsolem  43883  onexoegt  44085  oaordnrex  44136  omnord1ex  44145  omcl3g  44175  tfsconcatb0  44185  indthinc  50388  indthincALT  50389  prsthinc  50390  setc1oid  50421  funcsetc1ocl  50422  funcsetc1o  50423  isinito2lem  50424  isinito4  50473  setc1onsubc  50528