Theorem nnord 7406

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

Syntax hints:   → wi 4   ∈ wcel 2050  Ord word 6030  Oncon0 6031  ωcom 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pr 5187  ax-un 7281

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-tp 4447  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-tr 5032  df-eprel 5318  df-po 5327  df-so 5328  df-fr 5367  df-we 5369  df-ord 6034  df-on 6035  df-lim 6036  df-suc 6037  df-om 7399

This theorem is referenced by:  nnlim  7411  nnsuc  7415  nnaordi  8047  nnaord  8048  nnaword  8056  nnmord  8061  nnmwordi  8064  nnawordex  8066  omsmo  8083  phplem1  8494  phplem2  8495  phplem3  8496  phplem4  8497  php  8499  php4  8502  nndomo  8509  ominf  8527  isinf  8528  pssnn  8533  dif1en  8548  unblem1  8567  isfinite2  8573  unfilem1  8579  inf3lem5  8891  inf3lem6  8892  cantnfp1lem2  8938  cantnfp1lem3  8939  dif1card  9232  pwsdompw  9426  ackbij1lem5  9446  ackbij1lem14  9455  ackbij1lem16  9457  ackbij1b  9461  ackbij2  9465  sornom  9499  infpssrlem4  9528  infpssrlem5  9529  fin23lem26  9547  fin23lem23  9548  isf32lem2  9576  isf32lem3  9577  isf32lem4  9578  domtriomlem  9664  axdc3lem2  9673  axdc3lem4  9675  canthp1lem2  9875  elni2  10099  piord  10102  addnidpi  10123  indpi  10129  om2uzf1oi  13139  fzennn  13154  hashp1i  13580  bnj529  31660  bnj1098  31703  bnj570  31824  bnj594  31831  bnj580  31832  bnj967  31864  bnj1001  31877  bnj1053  31893  bnj1071  31894  hfun  33160  finminlem  33187  finxpsuclem  34119  finxpsuc  34120  wepwso  39039