Theorem nnord 4733

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

Syntax hints:   → wi 4   ∈ wcel 2203  Ord word 4482  Oncon0 4483  ωcom 4711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-nul 4235  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-iinf 4709

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-nul 3508  df-pw 3670  df-sn 3694  df-pr 3695  df-uni 3914  df-int 3949  df-tr 4208  df-iord 4486  df-on 4488  df-suc 4491  df-iom 4712

This theorem is referenced by:  nnsucsssuc  6724  nnsucuniel  6727  nntri1  6728  nnsseleq  6733  nntr2  6735  phplem1  7105  phplem2  7106  phplem3  7107  phplem4  7108  phplem4dom  7115  nndomo  7117  1ndom2  7118  dif1en  7135  nnwetri  7175  unsnfi  7178  ctmlemr  7398  nnnninf  7416  nnnninfeq  7418  nnnninfeq2  7419  nninfisol  7423  piord  7625  addnidpig  7650  archnqq  7731  frecfzennn  10787  hashp1i  11173  ennnfonelemk  13143  ennnfonelemg  13146  ennnfonelemhf1o  13156  ennnfonelemhom  13158  ctinfom  13171  3dom  16754  nnsf  16775  peano4nninf  16776  nninfsellemeq  16784  nnnninfex  16792