Theorem nnord 7582

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

Syntax hints:   → wi 4   ∈ wcel 2110  Ord word 6185  Oncon0 6186  ωcom 7574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-tr 5166  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-om 7575

This theorem is referenced by:  nnlim  7587  nnsuc  7591  omsucne  7592  nnaordi  8238  nnaord  8239  nnaword  8247  nnmord  8252  nnmwordi  8255  nnawordex  8257  omsmo  8275  phplem1  8690  phplem2  8691  phplem3  8692  phplem4  8693  php  8695  php4  8698  nndomo  8706  ominf  8724  isinf  8725  pssnn  8730  dif1en  8745  unblem1  8764  isfinite2  8770  unfilem1  8776  inf3lem5  9089  inf3lem6  9090  cantnfp1lem2  9136  cantnfp1lem3  9137  dif1card  9430  pwsdompw  9620  ackbij1lem5  9640  ackbij1lem14  9649  ackbij1lem16  9651  ackbij1b  9655  ackbij2  9659  sornom  9693  infpssrlem4  9722  infpssrlem5  9723  fin23lem26  9741  fin23lem23  9742  isf32lem2  9770  isf32lem3  9771  isf32lem4  9772  domtriomlem  9858  axdc3lem2  9867  axdc3lem4  9869  canthp1lem2  10069  elni2  10293  piord  10296  addnidpi  10317  indpi  10323  om2uzf1oi  13315  fzennn  13330  hashp1i  13758  bnj529  32007  bnj1098  32050  bnj570  32172  bnj594  32179  bnj580  32180  bnj967  32212  bnj1001  32226  bnj1053  32243  bnj1071  32244  hfun  33634  finminlem  33661  finxpsuclem  34672  finxpsuc  34673  wepwso  39636  nndomog  39890