Theorem nnord 7035

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

Syntax hints:   → wi 4   ∈ wcel 1987  Ord word 5691  Oncon0 5692  ωcom 7027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877  ax-un 6914

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-tr 4723  df-eprel 4995  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-om 7028

This theorem is referenced by:  nnlim  7040  nnsuc  7044  nnaordi  7658  nnaord  7659  nnaword  7667  nnmord  7672  nnmwordi  7675  nnawordex  7677  omsmo  7694  phplem1  8099  phplem2  8100  phplem3  8101  phplem4  8102  php  8104  php4  8107  nndomo  8114  ominf  8132  isinf  8133  pssnn  8138  dif1en  8153  unblem1  8172  isfinite2  8178  unfilem1  8184  inf3lem5  8489  inf3lem6  8490  cantnfp1lem2  8536  cantnfp1lem3  8537  dif1card  8793  pwsdompw  8986  ackbij1lem5  9006  ackbij1lem14  9015  ackbij1lem16  9017  ackbij1b  9021  ackbij2  9025  sornom  9059  infpssrlem4  9088  infpssrlem5  9089  fin23lem26  9107  fin23lem23  9108  isf32lem2  9136  isf32lem3  9137  isf32lem4  9138  domtriomlem  9224  axdc3lem2  9233  axdc3lem4  9235  canthp1lem2  9435  elni2  9659  piord  9662  addnidpi  9683  indpi  9689  om2uzf1oi  12708  fzennn  12723  hashp1i  13147  bnj529  30572  bnj1098  30615  bnj570  30736  bnj594  30743  bnj580  30744  bnj967  30776  bnj1001  30789  bnj1053  30805  bnj1071  30806  hfun  31980  finminlem  32007  finxpsuclem  32905  finxpsuc  32906  wepwso  37132