Theorem 0lt1o 8428

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  ∅c0 4282  1_oc1o 8387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-un 3903  df-nul 4283  df-sn 4578  df-suc 6320  df-1o 8394

This theorem is referenced by:  dif20el  8429  oe1m  8469  oen0  8510  oeoa  8521  oeoe  8523  isfin4p1  10217  fin1a2lem4  10305  1lt2pi  10807  indpi  10809  sadcp1  16373  vr1cl2  22124  fvcoe1  22139  vr1cl  22149  subrgvr1cl  22195  coe1mul2lem1  22200  coe1tm  22206  ply1coe  22233  evl1var  22271  evls1var  22273  rhmply1vr1  22322  xkofvcn  23619  fineqvnttrclse  35216  pw2f1ocnv  43194  wepwsolem  43199  onexoegt  43401  oaordnrex  43452  omnord1ex  43461  omcl3g  43491  tfsconcatb0  43501  indthinc  49623  indthincALT  49624  prsthinc  49625  setc1oid  49656  funcsetc1ocl  49657  funcsetc1o  49658  isinito2lem  49659  isinito4  49708  setc1onsubc  49763