![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1onn | Structured version Visualization version GIF version |
Description: One is a natural number. (Contributed by NM, 29-Oct-1995.) |
Ref | Expression |
---|---|
1onn | ⊢ 1o ∈ ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o 7845 | . 2 ⊢ 1o = suc ∅ | |
2 | peano1 7365 | . . 3 ⊢ ∅ ∈ ω | |
3 | peano2 7366 | . . 3 ⊢ (∅ ∈ ω → suc ∅ ∈ ω) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ suc ∅ ∈ ω |
5 | 1, 4 | eqeltri 2855 | 1 ⊢ 1o ∈ ω |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ∅c0 4141 suc csuc 5980 ωcom 7345 1oc1o 7838 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pr 5140 ax-un 7228 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-tr 4990 df-eprel 5268 df-po 5276 df-so 5277 df-fr 5316 df-we 5318 df-ord 5981 df-on 5982 df-lim 5983 df-suc 5984 df-om 7346 df-1o 7845 |
This theorem is referenced by: 2onn 8006 oaabs2 8011 omabs 8013 nnm2 8015 nnneo 8017 nneob 8018 snfi 8328 snnen2o 8439 1sdom2 8449 1sdom 8453 unxpdom2 8458 en1eqsn 8480 en2 8486 pwfi 8551 wofib 8741 oancom 8847 cnfcom3clem 8901 djurf1o 9074 card1 9129 pm54.43lem 9160 en2eleq 9166 en2other2 9167 infxpenlem 9171 infxpenc2lem1 9177 sdom2en01 9461 cfpwsdom 9743 canthp1lem2 9812 gchcda1 9815 pwxpndom2 9824 pwcdandom 9826 1pi 10042 1lt2pi 10064 indpi 10066 hash2 13511 hash1snb 13525 f1otrspeq 18254 pmtrf 18262 pmtrmvd 18263 pmtrfinv 18268 lt6abl 18686 isnzr2 19664 vr1cl 19987 ply1coe 20066 frgpcyg 20321 isppw 25296 bnj906 31603 finxpreclem1 33824 finxpreclem2 33825 finxp1o 33827 finxpreclem4 33829 finxp2o 33834 |
Copyright terms: Public domain | W3C validator |