Theorem nnon 7870

Description: A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)

Assertion

Ref	Expression
nnon	⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Proof of Theorem nnon

Step	Hyp	Ref	Expression
1		omsson 7868	. 2 ⊢ ω ⊆ On
2	1	sseli 3934	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Oncon0 6364  ωcom 7864

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-ss 3923  df-om 7865

This theorem is used by:  nnoni  7871  nnord  7872  peano4  7891  findsg  7896  onasuc  8515  onmsuc  8516  nna0  8592  nnm0  8593  nnasuc  8594  nnmsuc  8595  nnesuc  8596  nnecl  8601  nnawordi  8609  nnmword  8621  nnawordex  8625  nnaordex  8626  oaabslem  8635  oaabs  8636  oaabs2  8637  omabslem  8638  omabs  8639  nnneo  8643  nneob  8644  naddoa  8691  omnaddcl  8692  dif1ennn  9150  findcard2  9152  onfin2  9204  nndomo  9205  findcard3  9246  dffi3  9394  card2inf  9520  elom3  9620  cantnfp1lem3  9652  cnfcomlem  9671  cnfcom  9672  cnfcom3  9676  ttrcltr  9688  ttrclselem1  9697  ttrclselem2  9698  finnum  9946  cardnn  9961  nnsdomel  9988  harsucnn  9996  nnadjuALT  10194  ficardun2  10197  ackbij1lem15  10228  ackbij2lem2  10234  ackbij2lem3  10235  ackbij2  10237  fin23lem22  10322  isf32lem5  10352  fin1a2lem4  10398  fin1a2lem9  10403  pwfseqlem3  10656  winainflem  10689  wunr1om  10715  tskr1om  10763  grothomex  10825  pion  10875  om2uzlt2i  14001  madefi  28137  oldfi  28138  precsexlem3  28433  precsexlem4  28434  precsexlem5  28435  om2noseqlt  28523  om2noseqlt2  28524  constrfin  34176  constrextdg2lem  34178  constrext2chnlem  34180  constrfiss  34181  constrllcllem  34182  constrlccllem  34183  constrcccllem  34184  constrcn  34190  constrcjcl  34198  bnj168  35160  fineqvnttrclselem1  35567  fineqvnttrclselem2  35568  fineqvnttrclse  35570  kardnnfi  35615  satfvsuc  35866  satf0suc  35881  sat1el2xp  35884  fmlasuc0  35889  elhf2  36680  findreccl  36997  ttctr  37037  ttcmin  37040  dfttc2g  37050  rdgeqoa  38049  exrecfnlem  38058  finxpreclem4  38073  finxpreclem6  38075  harinf  43794  onexoegt  44004  oaabsb  44054  nnoeomeqom  44072  cantnfub  44081  dflim5  44089  onmcl  44091  omabs2  44092  tfsconcat0b  44106  naddcnffo  44124  naddonnn  44155  naddwordnexlem0  44156  naddwordnexlem3  44159  oawordex3  44160  naddwordnexlem4  44161  omssrncard  44299  nna1iscard  44304  hashnnsuc  45762  hashnnm  45763  hashnnltb  45765