Theorem nnord 7869

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Ord word 6351  Oncon0 6352  ωcom 7861

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-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-ord 6355  df-on 6356  df-om 7862

This theorem is used by:  nnlim  7875  nnsuc  7879  omsucne  7880  omun  7883  nnaordi  8606  nnaord  8607  nnaword  8615  nnmord  8620  nnmwordi  8623  nnawordex  8625  nnaordex2  8627  omsmo  8646  eldifsucnn  8652  enrefnn  9053  pssnn  9163  unfi  9165  phplem2  9199  php  9201  php4  9204  nndomog  9207  onomeneq  9208  ominf  9234  isinf  9235  dif1ennnALT  9247  findcard3  9253  unblem1  9262  isfinite2  9268  unfilem1  9275  inf3lem5  9611  inf3lem6  9612  cantnfp1lem2  9658  cantnfp1lem3  9659  ttrcltr  9695  ttrclss  9699  dmttrcl  9700  rnttrcl  9701  ttrclselem2  9705  hfun  9879  dif1card  10046  nnadju  10233  pwsdompw  10238  ackbij1lem5  10258  ackbij1lem14  10267  ackbij1lem16  10269  ackbij1b  10273  ackbij2  10277  sornom  10312  infpssrlem4  10341  infpssrlem5  10342  fin23lem26  10360  fin23lem23  10361  isf32lem2  10389  isf32lem3  10390  isf32lem4  10391  domtriomlem  10477  axdc3lem2  10486  axdc3lem4  10488  canthp1lem2  10695  elni2  10919  piord  10922  addnidpi  10943  indpi  10949  om2uzf1oi  14050  fzennn  14065  hashp1i  14500  om2noseqf1o  28606  bnj529  35292  bnj1098  35334  bnj570  35455  bnj594  35462  bnj580  35463  bnj967  35495  bnj1001  35509  bnj1053  35526  bnj1071  35527  fineqvnttrclselem2  35709  fineqvnttrclselem3  35710  nnuni  36407  finminlem  37022  mh-inf3f1  37245  finxpsuclem  38234  finxpsuc  38235  wepwso  43982  dflim5  44268  hashnnlt  45943