Theorem 0lt1o 8467

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 2761	. 2 ⊢ ∅ = ∅
2		el1o 8458	. 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅)
3	1, 2	mpbir 233	1 ⊢ ∅ ∈ 1o

Syntax hints:   = wceq 1559   ∈ wcel 2141  ∅c0 4283  1_oc1o 8424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3905  df-un 3907  df-nul 4284  df-sn 4580  df-suc 6347  df-1o 8431

This theorem is referenced by:  dif20el  8468  oe1m  8508  oen0  8550  oeoa  8561  oeoe  8563  isfin4p1  10266  fin1a2lem4  10354  1lt2pi  10857  indpi  10859  sadcp1  16480  vr1cl2  22243  fvcoe1  22257  vr1cl  22267  subrgvr1cl  22313  coe1mul2lem1  22318  coe1tm  22324  ply1coe  22349  evl1var  22387  evls1var  22389  rhmply1vr1  22435  xkofvcn  23732  selvply1rhmlema  33776  selvply1rhmlemb  33777  selvply1rhmlem1  33778  selvply1rhmlem2  33779  selvply1rhmlem4  33781  fineqvnttrclse  35381  pw2f1ocnv  43575  wepwsolem  43580  onexoegt  43782  oaordnrex  43833  omnord1ex  43842  omcl3g  43872  tfsconcatb0  43882  indthinc  50044  indthincALT  50045  prsthinc  50046  setc1oid  50077  funcsetc1ocl  50078  funcsetc1o  50079  isinito2lem  50080  isinito4  50129  setc1onsubc  50184