Theorem nnord 7226

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

Syntax hints:   → wi 4   ∈ wcel 2127  Ord word 5871  Oncon0 5872  ωcom 7218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pr 5043  ax-un 7102

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-tr 4893  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-om 7219

This theorem is referenced by:  nnlim  7231  nnsuc  7235  nnaordi  7855  nnaord  7856  nnaword  7864  nnmord  7869  nnmwordi  7872  nnawordex  7874  omsmo  7891  phplem1  8292  phplem2  8293  phplem3  8294  phplem4  8295  php  8297  php4  8300  nndomo  8307  ominf  8325  isinf  8326  pssnn  8331  dif1en  8346  unblem1  8365  isfinite2  8371  unfilem1  8377  inf3lem5  8690  inf3lem6  8691  cantnfp1lem2  8737  cantnfp1lem3  8738  dif1card  8994  pwsdompw  9189  ackbij1lem5  9209  ackbij1lem14  9218  ackbij1lem16  9220  ackbij1b  9224  ackbij2  9228  sornom  9262  infpssrlem4  9291  infpssrlem5  9292  fin23lem26  9310  fin23lem23  9311  isf32lem2  9339  isf32lem3  9340  isf32lem4  9341  domtriomlem  9427  axdc3lem2  9436  axdc3lem4  9438  canthp1lem2  9638  elni2  9862  piord  9865  addnidpi  9886  indpi  9892  om2uzf1oi  12917  fzennn  12932  hashp1i  13354  bnj529  31089  bnj1098  31132  bnj570  31253  bnj594  31260  bnj580  31261  bnj967  31293  bnj1001  31306  bnj1053  31322  bnj1071  31323  hfun  32562  finminlem  32589  finxpsuclem  33516  finxpsuc  33517  wepwso  38084