Theorem 0lt1o 7584

Description: Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)

Assertion

Ref	Expression
0lt1o	⊢ ∅ ∈ 1𝑜

Proof of Theorem 0lt1o

Step	Hyp	Ref	Expression
1		eqid 2622	. 2 ⊢ ∅ = ∅
2		el1o 7579	. 2 ⊢ (∅ ∈ 1𝑜 ↔ ∅ = ∅)
3	1, 2	mpbir 221	1 ⊢ ∅ ∈ 1𝑜

Syntax hints:   = wceq 1483   ∈ wcel 1990  ∅c0 3915  1_𝑜c1o 7553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-nul 3916  df-sn 4178  df-suc 5729  df-1o 7560

This theorem is referenced by:  dif20el  7585  oe1m  7625  oen0  7666  oeoa  7677  oeoe  7679  isfin4-3  9137  fin1a2lem4  9225  1lt2pi  9727  indpi  9729  sadcp1  15177  vr1cl2  19563  fvcoe1  19577  vr1cl  19587  subrgvr1cl  19632  coe1mul2lem1  19637  coe1tm  19643  ply1coe  19666  evl1var  19700  evls1var  19702  xkofvcn  21487  pw2f1ocnv  37604  wepwsolem  37612