Theorem 0lt1o 8517

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  ∅c0 4277  1_oc1o 8474

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4046  df-un 4150  df-nul 4278  df-sn 4585  df-suc 6370  df-1o 8481

This theorem is used by:  dif20el  8518  oe1m  8558  oen0  8600  oeoa  8611  oeoe  8613  isfin4p1  10398  fin1a2lem4  10486  1lt2pi  10995  indpi  10997  sadcp1  16632  vr1cl2  22518  fvcoe1  22532  vr1cl  22542  subrgvr1cl  22588  coe1mul2lem1  22593  coe1tm  22599  ply1coe  22623  evl1var  22661  evls1var  22663  rhmply1vr1  22709  xkofvcn  24010  selvply1rhmlema  34198  selvply1rhmlemb  34199  selvply1rhmlem1  34200  selvply1rhmlem2  34201  selvply1rhmlem4  34203  fineqvnttrclse  35850  pw2f1ocnv  44151  wepwsolem  44156  onexoegt  44353  oaordnrex  44404  omnord1ex  44413  omcl3g  44443  tfsconcatb0  44453  indthinc  50704  indthincALT  50705  prsthinc  50706  setc1oid  50737  funcsetc1ocl  50738  funcsetc1o  50739  isinito2lem  50740  isinito4  50792  setc1onsubc  50847  par2diag  50887  fuconuniqlem  50888  fuconuniqvalslem  50890