Theorem nnord 7695

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 7693	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
2		eloni 6261	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ ω → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2108  Ord word 6250  Oncon0 6251  ωcom 7687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-tr 5188  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-ord 6254  df-on 6255  df-om 7688

This theorem is referenced by:  nnlim  7701  nnsuc  7705  omsucne  7706  nnaordi  8411  nnaord  8412  nnaword  8420  nnmord  8425  nnmwordi  8428  nnawordex  8430  omsmo  8448  enrefnn  8791  phplem1  8892  phplem2  8893  phplem3  8894  phplem4  8895  php  8897  php4  8900  nndomog  8904  dif1enlem  8905  pssnn  8913  unfi  8917  ominf  8964  isinf  8965  pssnnOLD  8969  dif1enALT  8980  unblem1  8996  isfinite2  9002  unfilem1  9008  inf3lem5  9320  inf3lem6  9321  cantnfp1lem2  9367  cantnfp1lem3  9368  dif1card  9697  nnadju  9884  pwsdompw  9891  ackbij1lem5  9911  ackbij1lem14  9920  ackbij1lem16  9922  ackbij1b  9926  ackbij2  9930  sornom  9964  infpssrlem4  9993  infpssrlem5  9994  fin23lem26  10012  fin23lem23  10013  isf32lem2  10041  isf32lem3  10042  isf32lem4  10043  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  canthp1lem2  10340  elni2  10564  piord  10567  addnidpi  10588  indpi  10594  om2uzf1oi  13601  fzennn  13616  hashp1i  14046  bnj529  32621  bnj1098  32663  bnj570  32785  bnj594  32792  bnj580  32793  bnj967  32825  bnj1001  32839  bnj1053  32856  bnj1071  32857  nnuni  33595  eldifsucnn  33597  ttrcltr  33702  ttrclss  33706  dmttrcl  33707  rnttrcl  33708  ttrclselem2  33712  hfun  34407  finminlem  34434  finxpsuclem  35495  finxpsuc  35496  wepwso  40784