Theorem 0lt1o 8431

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  ∅c0 4285  1_oc1o 8390

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 2708  ax-nul 5251

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286  df-sn 4581  df-suc 6323  df-1o 8397

This theorem is referenced by:  dif20el  8432  oe1m  8472  oen0  8514  oeoa  8525  oeoe  8527  isfin4p1  10225  fin1a2lem4  10313  1lt2pi  10816  indpi  10818  sadcp1  16382  vr1cl2  22133  fvcoe1  22148  vr1cl  22158  subrgvr1cl  22204  coe1mul2lem1  22209  coe1tm  22215  ply1coe  22242  evl1var  22280  evls1var  22282  rhmply1vr1  22331  xkofvcn  23628  fineqvnttrclse  35280  pw2f1ocnv  43279  wepwsolem  43284  onexoegt  43486  oaordnrex  43537  omnord1ex  43546  omcl3g  43576  tfsconcatb0  43586  indthinc  49707  indthincALT  49708  prsthinc  49709  setc1oid  49740  funcsetc1ocl  49741  funcsetc1o  49742  isinito2lem  49743  isinito4  49792  setc1onsubc  49847