![]() |
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 7303 | . 2 ⊢ ω ⊆ On | |
2 | 1 | sseli 3794 | 1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2157 Oncon0 5941 ωcom 7299 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pr 5097 ax-un 7183 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-sbc 3634 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-tp 4373 df-op 4375 df-uni 4629 df-br 4844 df-opab 4906 df-tr 4946 df-eprel 5225 df-po 5233 df-so 5234 df-fr 5271 df-we 5273 df-ord 5944 df-on 5945 df-lim 5946 df-suc 5947 df-om 7300 |
This theorem is referenced by: nnoni 7306 nnord 7307 peano4 7322 findsg 7327 onasuc 7848 onmsuc 7849 nna0 7924 nnm0 7925 nnasuc 7926 nnmsuc 7927 nnesuc 7928 nnecl 7933 nnawordi 7941 nnmword 7953 nnawordex 7957 nnaordex 7958 oaabslem 7963 oaabs 7964 oaabs2 7965 omabslem 7966 omabs 7967 nnneo 7971 nneob 7972 onfin2 8394 findcard3 8445 dffi3 8579 card2inf 8702 elom3 8795 cantnfp1lem3 8827 cnfcomlem 8846 cnfcom 8847 cnfcom3 8851 finnum 9060 cardnn 9075 nnsdomel 9102 nnacda 9311 ficardun2 9313 ackbij1lem15 9344 ackbij2lem2 9350 ackbij2lem3 9351 ackbij2 9353 fin23lem22 9437 isf32lem5 9467 fin1a2lem4 9513 fin1a2lem9 9518 pwfseqlem3 9770 winainflem 9803 wunr1om 9829 tskr1om 9877 grothomex 9939 pion 9989 om2uzlt2i 13005 bnj168 31316 elhf2 32795 findreccl 32960 rdgeqoa 33716 finxpreclem4 33729 finxpreclem6 33731 harinf 38386 |
Copyright terms: Public domain | W3C validator |