Theorem nnord 7720

Description: A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)

Assertion

Ref	Expression
nnord	⊢ (𝐴 ∈ ω → Ord 𝐴)

Proof of Theorem nnord

Step	Hyp	Ref	Expression
1		nnon 7718	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
2		eloni 6276	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ ω → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2106  Ord word 6265  Oncon0 6266  ωcom 7712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-tr 5192  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269  df-on 6270  df-om 7713

This theorem is referenced by:  nnlim  7726  nnsuc  7730  omsucne  7731  nnaordi  8449  nnaord  8450  nnaword  8458  nnmord  8463  nnmwordi  8466  nnawordex  8468  omsmo  8488  eldifsucnn  8494  enrefnn  8837  dif1enlem  8943  pssnn  8951  unfi  8955  phplem2  8991  php  8993  php4  8996  nndomog  8999  phplem1OLD  9000  phplem2OLD  9001  phplem3OLD  9002  phplem4OLD  9003  phpOLD  9005  nndomogOLD  9009  onomeneq  9011  ominf  9035  isinf  9036  pssnnOLD  9040  dif1enALT  9050  unblem1  9066  isfinite2  9072  unfilem1  9078  inf3lem5  9390  inf3lem6  9391  cantnfp1lem2  9437  cantnfp1lem3  9438  ttrcltr  9474  ttrclss  9478  dmttrcl  9479  rnttrcl  9480  ttrclselem2  9484  dif1card  9766  nnadju  9953  pwsdompw  9960  ackbij1lem5  9980  ackbij1lem14  9989  ackbij1lem16  9991  ackbij1b  9995  ackbij2  9999  sornom  10033  infpssrlem4  10062  infpssrlem5  10063  fin23lem26  10081  fin23lem23  10082  isf32lem2  10110  isf32lem3  10111  isf32lem4  10112  domtriomlem  10198  axdc3lem2  10207  axdc3lem4  10209  canthp1lem2  10409  elni2  10633  piord  10636  addnidpi  10657  indpi  10663  om2uzf1oi  13673  fzennn  13688  hashp1i  14118  bnj529  32721  bnj1098  32763  bnj570  32885  bnj594  32892  bnj580  32893  bnj967  32925  bnj1001  32939  bnj1053  32956  bnj1071  32957  nnuni  33692  hfun  34480  finminlem  34507  finxpsuclem  35568  finxpsuc  35569  wepwso  40868