Theorem nnord 7804

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

Syntax hints:   → wi 4   ∈ wcel 2111  Ord word 6305  Oncon0 6306  ωcom 7796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rab 3396  df-v 3438  df-ss 3914  df-uni 4857  df-tr 5197  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-ord 6309  df-on 6310  df-om 7797

This theorem is referenced by:  nnlim  7810  nnsuc  7814  omsucne  7815  omun  7818  nnaordi  8533  nnaord  8534  nnaword  8542  nnmord  8547  nnmwordi  8550  nnawordex  8552  nnaordex2  8554  omsmo  8573  eldifsucnn  8579  enrefnn  8968  pssnn  9078  unfi  9080  phplem2  9114  php  9116  php4  9119  nndomog  9122  onomeneq  9123  ominf  9148  isinf  9149  dif1ennnALT  9161  findcard3  9167  unblem1  9176  isfinite2  9182  unfilem1  9189  inf3lem5  9522  inf3lem6  9523  cantnfp1lem2  9569  cantnfp1lem3  9570  ttrcltr  9606  ttrclss  9610  dmttrcl  9611  rnttrcl  9612  ttrclselem2  9616  dif1card  9901  nnadju  10089  pwsdompw  10094  ackbij1lem5  10114  ackbij1lem14  10123  ackbij1lem16  10125  ackbij1b  10129  ackbij2  10133  sornom  10168  infpssrlem4  10197  infpssrlem5  10198  fin23lem26  10216  fin23lem23  10217  isf32lem2  10245  isf32lem3  10246  isf32lem4  10247  domtriomlem  10333  axdc3lem2  10342  axdc3lem4  10344  canthp1lem2  10544  elni2  10768  piord  10771  addnidpi  10792  indpi  10798  om2uzf1oi  13860  fzennn  13875  hashp1i  14310  om2noseqf1o  28231  bnj529  34753  bnj1098  34795  bnj570  34917  bnj594  34924  bnj580  34925  bnj967  34957  bnj1001  34971  bnj1053  34988  bnj1071  34989  fineqvnttrclselem2  35142  fineqvnttrclselem3  35143  nnuni  35771  hfun  36222  finminlem  36362  finxpsuclem  37441  finxpsuc  37442  wepwso  43135  dflim5  43421