Theorem nnord 7874

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ord word 6356  Oncon0 6357  ωcom 7866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rab 3421  df-v 3466  df-ss 3948  df-uni 4889  df-tr 5235  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6360  df-on 6361  df-om 7867

This theorem is referenced by:  nnlim  7880  nnsuc  7884  omsucne  7885  omun  7888  nnaordi  8635  nnaord  8636  nnaword  8644  nnmord  8649  nnmwordi  8652  nnawordex  8654  nnaordex2  8656  omsmo  8675  eldifsucnn  8681  enrefnn  9066  dif1enlemOLD  9176  pssnn  9187  unfi  9190  phplem2  9224  php  9226  php4  9229  nndomog  9232  phplem1OLD  9233  phplem2OLD  9234  phplem3OLD  9235  phpOLD  9236  nndomogOLD  9240  onomeneq  9242  ominf  9271  ominfOLD  9272  isinf  9273  isinfOLD  9274  dif1ennnALT  9288  findcard3  9295  unblem1  9305  isfinite2  9311  unfilem1  9320  inf3lem5  9651  inf3lem6  9652  cantnfp1lem2  9698  cantnfp1lem3  9699  ttrcltr  9735  ttrclss  9739  dmttrcl  9740  rnttrcl  9741  ttrclselem2  9745  dif1card  10029  nnadju  10217  pwsdompw  10222  ackbij1lem5  10242  ackbij1lem14  10251  ackbij1lem16  10253  ackbij1b  10257  ackbij2  10261  sornom  10296  infpssrlem4  10325  infpssrlem5  10326  fin23lem26  10344  fin23lem23  10345  isf32lem2  10373  isf32lem3  10374  isf32lem4  10375  domtriomlem  10461  axdc3lem2  10470  axdc3lem4  10472  canthp1lem2  10672  elni2  10896  piord  10899  addnidpi  10920  indpi  10926  om2uzf1oi  13976  fzennn  13991  hashp1i  14426  om2noseqf1o  28252  bnj529  34777  bnj1098  34819  bnj570  34941  bnj594  34948  bnj580  34949  bnj967  34981  bnj1001  34995  bnj1053  35012  bnj1071  35013  nnuni  35749  hfun  36201  finminlem  36341  finxpsuclem  37420  finxpsuc  37421  wepwso  43042  dflim5  43328