Theorem nnon 7868

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 7866	. 2 ⊢ ω ⊆ On
2	1	sseli 3927	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Oncon0 6357  ωcom 7862

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3916  df-om 7863

This theorem is used by:  nnoni  7869  nnord  7870  peano4  7889  findsg  7894  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  9157  findcard2  9159  onfin2  9211  nndomo  9212  findcard3  9253  dffi3  9401  card2inf  9527  elom3  9627  cantnfp1lem3  9659  cnfcomlem  9678  cnfcom  9679  cnfcom3  9683  ttrcltr  9695  ttrclselem1  9704  ttrclselem2  9705  finnum  9953  cardnn  9968  nnsdomel  9995  harsucnn  10003  nnadjuALT  10201  ficardun2  10204  ackbij1lem15  10235  ackbij2lem2  10241  ackbij2lem3  10242  ackbij2  10244  fin23lem22  10329  isf32lem5  10359  fin1a2lem4  10405  fin1a2lem9  10410  pwfseqlem3  10669  winainflem  10702  wunr1om  10728  tskr1om  10776  grothomex  10838  pion  10888  om2uzlt2i  14015  madefi  28178  oldfi  28179  precsexlem3  28474  precsexlem4  28475  precsexlem5  28476  om2noseqlt  28564  om2noseqlt2  28565  constrfin  34256  constrextdg2lem  34258  constrext2chnlem  34260  constrfiss  34261  constrllcllem  34262  constrlccllem  34263  constrcccllem  34264  constrcn  34270  constrcjcl  34278  bnj168  35240  fineqvnttrclselem1  35647  fineqvnttrclselem2  35648  fineqvnttrclse  35650  kardnnfi  35695  satfvsuc  35940  satf0suc  35955  sat1el2xp  35958  fmlasuc0  35963  elhf2  36755  findreccl  37072  ttctr  37112  ttcmin  37115  dfttc2g  37125  rdgeqoa  38124  exrecfnlem  38133  finxpreclem4  38148  finxpreclem6  38150  harinf  43875  onexoegt  44085  oaabsb  44135  nnoeomeqom  44153  cantnfub  44162  dflim5  44170  onmcl  44172  omabs2  44173  tfsconcat0b  44187  naddcnffo  44205  naddonnn  44236  naddwordnexlem0  44237  naddwordnexlem3  44240  oawordex3  44241  naddwordnexlem4  44242  omssrncard  44380  nna1iscard  44385  hashnnsuc  45843  hashnnm  45844  hashnnltb  45846