Theorem 1n0 8478

Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
1n0	⊢ 1o ≠ ∅

Proof of Theorem 1n0

Step	Hyp	Ref	Expression
1		df-1o 8459	. 2 ⊢ 1o = suc ∅
2		nsuceq0 6447	. 2 ⊢ suc ∅ ≠ ∅
3	1, 2	eqnetri 3027	1 ⊢ 1o ≠ ∅

This proof depends on syntax axioms:   ≠ wne 2957  ∅c0 4282  suc csuc 6363  1_oc1o 8452

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-un 3907  df-nul 4283  df-sn 4588  df-suc 6367  df-1o 8459

This theorem is used by:  nlim1  8480  xp01disj  8482  xp01disjl  8483  enpr2d  9059  map2xp  9149  snnen2o  9219  0sdom1dom  9220  sdom1  9224  rex2dom  9227  1sdom2dom  9228  unxpdom2  9234  sucxpdom  9235  ssttrcl  9698  ttrclselem2  9709  djuin  9927  eldju2ndl  9933  updjudhcoinrg  9942  card1  9977  pm54.43lem  10009  cflim2  10269  isfin4p1  10321  dcomex  10453  pwcfsdom  10596  cfpwsdom  10597  canthp1lem2  10666  wunex2  10751  1pi  10896  fnpr2o  17649  fnpr2ob  17650  fvpr0o  17651  fvpr1o  17652  fvprif  17653  xpsfrnel  17654  setcepi  18183  setc2obas  18189  degenmgmnfn  19055  degenmgm  19056  degenmgm2  19059  frgpuptinv  19904  frgpup3lem  19910  frgpnabllem1  20006  dmdprdpr  20184  dprdpr  20185  coe1mul2lem1  22499  2ndcdisj  23688  xpstopnlem1  24041  ltsval2  27900  nosgnn0  27902  ltsintdifex  27905  ltsres  27906  nogesgn1ores  27918  ltssolem1  27919  nosepnelem  27923  nogt01o  27940  noinfbnd1lem3  27969  noinfbnd2lem1  27974  bnj906  35447  gonan0  35979  gonar  35982  fmla0disjsuc  35985  rankeq1o  36759  onint1  37076  bj-disjsn01  37704  bj-0nel1  37705  bj-1nel0  37706  bj-pr21val  37765  bj-pr22val  37771  finxp1o  38154  finxp2o  38161  domalom  38166  wepwsolem  43891  onov0suclim  44123  clsk3nimkb  44888  clsk1indlem4  44892  clsk1indlem1  44893  nelsubc3  50005  prsthinc  50398  prstchom  50496  prstchom2ALT  50498