Theorem 0lt1o 8550

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  ∅c0 4281  1_oc1o 8507

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5266

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-suc 6394  df-1o 8514

This theorem is used by:  dif20el  8551  oe1m  8591  oen0  8633  oeoa  8644  oeoe  8646  isfin4p1  10432  fin1a2lem4  10520  1lt2pi  11029  indpi  11031  sadcp1  16669  vr1cl2  22566  fvcoe1  22580  vr1cl  22590  subrgvr1cl  22636  coe1mul2lem1  22641  coe1tm  22647  ply1coe  22671  evl1var  22709  evls1var  22711  rhmply1vr1  22757  xkofvcn  24058  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem1  34263  selvply1rhmlem2  34264  selvply1rhmlem4  34266  fineqvnttrclse  35933  pw2f1ocnv  44310  wepwsolem  44315  onexoegt  44507  oaordnrex  44558  omnord1ex  44567  omcl3g  44597  tfsconcatb0  44607  indthinc  50928  indthincALT  50929  prsthinc  50930  setc1oid  50961  funcsetc1ocl  50962  funcsetc1o  50963  isinito2lem  50964  isinito4  51016  setc1onsubc  51071  par2diag  51111  fuconuniqlem  51112  fuconuniqvalslem  51114