Theorem 0lt1o 8485

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 2769	. 2 ⊢ ∅ = ∅
2		el1o 8476	. 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅)
3	1, 2	mpbir 234	1 ⊢ ∅ ∈ 1o

Syntax hints:   = wceq 1567   ∈ wcel 2149  ∅c0 4294  1_oc1o 8442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5268

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-un 3918  df-nul 4295  df-sn 4592  df-suc 6364  df-1o 8449

This theorem is referenced by:  dif20el  8486  oe1m  8526  oen0  8568  oeoa  8579  oeoe  8581  isfin4p1  10295  fin1a2lem4  10383  1lt2pi  10886  indpi  10888  sadcp1  16509  vr1cl2  22318  fvcoe1  22332  vr1cl  22342  subrgvr1cl  22388  coe1mul2lem1  22393  coe1tm  22399  ply1coe  22423  evl1var  22461  evls1var  22463  rhmply1vr1  22509  xkofvcn  23806  selvply1rhmlema  33849  selvply1rhmlemb  33850  selvply1rhmlem1  33851  selvply1rhmlem2  33852  selvply1rhmlem4  33854  fineqvnttrclse  35456  pw2f1ocnv  43651  wepwsolem  43656  onexoegt  43858  oaordnrex  43909  omnord1ex  43918  omcl3g  43948  tfsconcatb0  43958  indthinc  50120  indthincALT  50121  prsthinc  50122  setc1oid  50153  funcsetc1ocl  50154  funcsetc1o  50155  isinito2lem  50156  isinito4  50205  setc1onsubc  50260