![]() |
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 7440 | . 2 ⊢ ω ⊆ On | |
2 | 1 | sseli 3885 | 1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2081 Oncon0 6066 ωcom 7436 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pr 5221 ax-un 7319 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-tr 5064 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-we 5404 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-om 7437 |
This theorem is referenced by: nnoni 7443 nnord 7444 peano4 7460 findsg 7465 onasuc 8004 onmsuc 8005 nna0 8080 nnm0 8081 nnasuc 8082 nnmsuc 8083 nnesuc 8084 nnecl 8089 nnawordi 8097 nnmword 8109 nnawordex 8113 nnaordex 8114 oaabslem 8120 oaabs 8121 oaabs2 8122 omabslem 8123 omabs 8124 nnneo 8128 nneob 8129 onfin2 8556 findcard3 8607 dffi3 8741 card2inf 8865 elom3 8957 cantnfp1lem3 8989 cnfcomlem 9008 cnfcom 9009 cnfcom3 9013 finnum 9223 cardnn 9238 nnsdomel 9265 nnadju 9469 ficardun2 9471 ackbij1lem15 9502 ackbij2lem2 9508 ackbij2lem3 9509 ackbij2 9511 fin23lem22 9595 isf32lem5 9625 fin1a2lem4 9671 fin1a2lem9 9676 pwfseqlem3 9928 winainflem 9961 wunr1om 9987 tskr1om 10035 grothomex 10097 pion 10147 om2uzlt2i 13169 bnj168 31617 satfvsuc 32216 satf0suc 32231 sat1el2xp 32234 fmlasuc0 32239 elhf2 33245 findreccl 33410 rdgeqoa 34182 exrecfnlem 34191 finxpreclem4 34206 finxpreclem6 34208 harinf 39116 harsucnn 39388 |
Copyright terms: Public domain | W3C validator |