Theorem 0lt1o 8542

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∅c0 4333  1_oc1o 8499

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-suc 6390  df-1o 8506

This theorem is referenced by:  dif20el  8543  oe1m  8583  oen0  8624  oeoa  8635  oeoe  8637  isfin4p1  10355  fin1a2lem4  10443  1lt2pi  10945  indpi  10947  sadcp1  16492  vr1cl2  22194  fvcoe1  22209  vr1cl  22219  subrgvr1cl  22265  coe1mul2lem1  22270  coe1tm  22276  ply1coe  22302  evl1var  22340  evls1var  22342  rhmply1vr1  22391  xkofvcn  23692  pw2f1ocnv  43049  wepwsolem  43054  onexoegt  43256  oaordnrex  43308  omnord1ex  43317  omcl3g  43347  tfsconcatb0  43357  indthinc  49109  indthincALT  49110  prsthinc  49111