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

Syntax hints:   = wceq 1570   ∈ wcel 2143  ∅c0 4286  1_oc1o 8442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5269

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-un 3910  df-nul 4287  df-sn 4590  df-suc 6366  df-1o 8449

This theorem is referenced by:  dif20el  8486  oe1m  8526  oen0  8568  oeoa  8579  oeoe  8581  isfin4p1  10294  fin1a2lem4  10382  1lt2pi  10885  indpi  10887  sadcp1  16508  vr1cl2  22353  fvcoe1  22367  vr1cl  22377  subrgvr1cl  22423  coe1mul2lem1  22428  coe1tm  22434  ply1coe  22458  evl1var  22496  evls1var  22498  rhmply1vr1  22544  xkofvcn  23841  selvply1rhmlema  33908  selvply1rhmlemb  33909  selvply1rhmlem1  33910  selvply1rhmlem2  33911  selvply1rhmlem4  33913  fineqvnttrclse  35537  pw2f1ocnv  43764  wepwsolem  43769  onexoegt  43971  oaordnrex  44022  omnord1ex  44031  omcl3g  44061  tfsconcatb0  44071  indthinc  50240  indthincALT  50241  prsthinc  50242  setc1oid  50273  funcsetc1ocl  50274  funcsetc1o  50275  isinito2lem  50276  isinito4  50325  setc1onsubc  50380