Theorem 0lt1o 8506

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 2732	. 2 ⊢ ∅ = ∅
2		el1o 8497	. 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅)
3	1, 2	mpbir 230	1 ⊢ ∅ ∈ 1o

Syntax hints:   = wceq 1541   ∈ wcel 2106  ∅c0 4322  1_oc1o 8461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-un 3953  df-nul 4323  df-sn 4629  df-suc 6370  df-1o 8468

This theorem is referenced by:  dif20el  8507  oe1m  8547  oen0  8588  oeoa  8599  oeoe  8601  isfin4p1  10312  fin1a2lem4  10400  1lt2pi  10902  indpi  10904  sadcp1  16400  vr1cl2  21936  fvcoe1  21950  vr1cl  21960  subrgvr1cl  22004  coe1mul2lem1  22009  coe1tm  22015  ply1coe  22040  evl1var  22075  evls1var  22077  xkofvcn  23408  pw2f1ocnv  42078  wepwsolem  42086  onexoegt  42295  oaordnrex  42347  omnord1ex  42356  omcl3g  42386  tfsconcatb0  42396  indthinc  47760  indthincALT  47761  prsthinc  47762