![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nnord | Structured version Visualization version GIF version |
Description: A natural number is ordinal. (Contributed by NM, 17-Oct-1995.) |
Ref | Expression |
---|---|
nnord | ⊢ (𝐴 ∈ ω → Ord 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnon 7224 | . 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On) | |
2 | eloni 5882 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐴 ∈ ω → Ord 𝐴) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |