Theorem 0lt1o 8468

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∅c0 4296  1_oc1o 8427

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-un 3919  df-nul 4297  df-sn 4590  df-suc 6338  df-1o 8434

This theorem is referenced by:  dif20el  8469  oe1m  8509  oen0  8550  oeoa  8561  oeoe  8563  isfin4p1  10268  fin1a2lem4  10356  1lt2pi  10858  indpi  10860  sadcp1  16425  vr1cl2  22077  fvcoe1  22092  vr1cl  22102  subrgvr1cl  22148  coe1mul2lem1  22153  coe1tm  22159  ply1coe  22185  evl1var  22223  evls1var  22225  rhmply1vr1  22274  xkofvcn  23571  pw2f1ocnv  43026  wepwsolem  43031  onexoegt  43233  oaordnrex  43284  omnord1ex  43293  omcl3g  43323  tfsconcatb0  43333  indthinc  49451  indthincALT  49452  prsthinc  49453  setc1oid  49484  funcsetc1ocl  49485  funcsetc1o  49486  isinito2lem  49487  isinito4  49536  setc1onsubc  49591