Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nnon | Structured version Visualization version GIF version |
Description: A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.) |
Ref | Expression |
---|---|
nnon | ⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omsson 7583 | . 2 ⊢ ω ⊆ On | |
2 | 1 | sseli 3962 | 1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 Oncon0 6190 ωcom 7579 |
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 2157 ax-12 2173 ax-ext 2793 ax-sep 5202 ax-nul 5209 ax-pr 5329 ax-un 7460 |
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 3496 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4838 df-br 5066 df-opab 5128 df-tr 5172 df-eprel 5464 df-po 5473 df-so 5474 df-fr 5513 df-we 5515 df-ord 6193 df-on 6194 df-lim 6195 df-suc 6196 df-om 7580 |
This theorem is referenced by: nnoni 7586 nnord 7587 peano4 7603 findsg 7608 onasuc 8152 onmsuc 8153 nna0 8229 nnm0 8230 nnasuc 8231 nnmsuc 8232 nnesuc 8233 nnecl 8238 nnawordi 8246 nnmword 8258 nnawordex 8262 nnaordex 8263 oaabslem 8269 oaabs 8270 oaabs2 8271 omabslem 8272 omabs 8273 nnneo 8277 nneob 8278 onfin2 8709 findcard3 8760 dffi3 8894 card2inf 9018 elom3 9110 cantnfp1lem3 9142 cnfcomlem 9161 cnfcom 9162 cnfcom3 9166 finnum 9376 cardnn 9391 nnsdomel 9418 nnadju 9622 ficardun2 9624 ackbij1lem15 9655 ackbij2lem2 9661 ackbij2lem3 9662 ackbij2 9664 fin23lem22 9748 isf32lem5 9778 fin1a2lem4 9824 fin1a2lem9 9829 pwfseqlem3 10081 winainflem 10114 wunr1om 10140 tskr1om 10188 grothomex 10250 pion 10300 om2uzlt2i 13318 bnj168 32000 satfvsuc 32608 satf0suc 32623 sat1el2xp 32626 fmlasuc0 32631 elhf2 33636 findreccl 33801 rdgeqoa 34650 exrecfnlem 34659 finxpreclem4 34674 finxpreclem6 34676 harinf 39629 harsucnn 39901 |
Copyright terms: Public domain | W3C validator |