|   | 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 7892 | . 2 ⊢ ω ⊆ On | |
| 2 | 1 | sseli 3978 | 1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∈ wcel 2107 Oncon0 6383 ωcom 7888 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-ss 3967 df-om 7889 | 
| This theorem is referenced by: nnoni 7895 nnord 7896 peano4 7915 findsg 7920 onasuc 8567 onmsuc 8568 nna0 8643 nnm0 8644 nnasuc 8645 nnmsuc 8646 nnesuc 8647 nnecl 8652 nnawordi 8660 nnmword 8672 nnawordex 8676 nnaordex 8677 oaabslem 8686 oaabs 8687 oaabs2 8688 omabslem 8689 omabs 8690 nnneo 8694 nneob 8695 naddoa 8741 omnaddcl 8742 dif1ennn 9202 findcard2 9205 onfin2 9269 nndomo 9270 findcard3 9319 findcard3OLD 9320 dffi3 9472 card2inf 9596 elom3 9689 cantnfp1lem3 9721 cnfcomlem 9740 cnfcom 9741 cnfcom3 9745 ttrcltr 9757 ttrclselem1 9766 ttrclselem2 9767 finnum 9989 cardnn 10004 nnsdomel 10031 harsucnn 10039 nnadjuALT 10240 ficardun2 10243 ackbij1lem15 10274 ackbij2lem2 10280 ackbij2lem3 10281 ackbij2 10283 fin23lem22 10368 isf32lem5 10398 fin1a2lem4 10444 fin1a2lem9 10449 pwfseqlem3 10701 winainflem 10734 wunr1om 10760 tskr1om 10808 grothomex 10870 pion 10920 om2uzlt2i 13993 madefi 27951 oldfi 27952 precsexlem3 28234 precsexlem4 28235 precsexlem5 28236 om2noseqlt 28306 om2noseqlt2 28307 zs12bday 28425 constrfin 33788 constrextdg2lem 33790 bnj168 34745 satfvsuc 35367 satf0suc 35382 sat1el2xp 35385 fmlasuc0 35390 elhf2 36177 findreccl 36455 rdgeqoa 37372 exrecfnlem 37381 finxpreclem4 37396 finxpreclem6 37398 harinf 43051 onexoegt 43261 oaabsb 43312 nnoeomeqom 43330 cantnfub 43339 dflim5 43347 onmcl 43349 omabs2 43350 tfsconcat0b 43364 naddcnffo 43382 naddonnn 43413 naddwordnexlem0 43414 naddwordnexlem3 43417 oawordex3 43418 naddwordnexlem4 43419 omssrncard 43558 nna1iscard 43563 | 
| Copyright terms: Public domain | W3C validator |