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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  ∅c0 4286  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 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-un 3911  df-nul 4287  df-sn 4592  df-suc 6370  df-1o 8455

This theorem is used by:  dif20el  8492  oe1m  8532  oen0  8574  oeoa  8585  oeoe  8587  isfin4p1  10310  fin1a2lem4  10398  1lt2pi  10901  indpi  10903  sadcp1  16531  vr1cl2  22383  fvcoe1  22397  vr1cl  22407  subrgvr1cl  22453  coe1mul2lem1  22458  coe1tm  22464  ply1coe  22488  evl1var  22526  evls1var  22528  rhmply1vr1  22574  xkofvcn  23872  selvply1rhmlema  33948  selvply1rhmlemb  33949  selvply1rhmlem1  33950  selvply1rhmlem2  33951  selvply1rhmlem4  33953  fineqvnttrclse  35570  pw2f1ocnv  43797  wepwsolem  43802  onexoegt  44004  oaordnrex  44055  omnord1ex  44064  omcl3g  44094  tfsconcatb0  44104  indthinc  50273  indthincALT  50274  prsthinc  50275  setc1oid  50306  funcsetc1ocl  50307  funcsetc1o  50308  isinito2lem  50309  isinito4  50358  setc1onsubc  50413