Theorem 0lt1o 8516

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 2735	. 2 ⊢ ∅ = ∅
2		el1o 8507	. 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅)
3	1, 2	mpbir 231	1 ⊢ ∅ ∈ 1o

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∅c0 4308  1_oc1o 8473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-un 3931  df-nul 4309  df-sn 4602  df-suc 6358  df-1o 8480

This theorem is referenced by:  dif20el  8517  oe1m  8557  oen0  8598  oeoa  8609  oeoe  8611  isfin4p1  10329  fin1a2lem4  10417  1lt2pi  10919  indpi  10921  sadcp1  16474  vr1cl2  22128  fvcoe1  22143  vr1cl  22153  subrgvr1cl  22199  coe1mul2lem1  22204  coe1tm  22210  ply1coe  22236  evl1var  22274  evls1var  22276  rhmply1vr1  22325  xkofvcn  23622  pw2f1ocnv  43061  wepwsolem  43066  onexoegt  43268  oaordnrex  43319  omnord1ex  43328  omcl3g  43358  tfsconcatb0  43368  indthinc  49348  indthincALT  49349  prsthinc  49350  setc1oid  49380  funcsetc1ocl  49381  funcsetc1o  49382  isinito2lem  49383  setc1onsubc  49479