![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > peano2nn | Structured version Visualization version GIF version |
Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
peano2nn | ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frfnom 7872 | . . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω | |
2 | fvelrnb 6553 | . . . 4 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω → (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) ↔ ∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴)) | |
3 | 1, 2 | ax-mp 5 | . . 3 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) ↔ ∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴) |
4 | ovex 7006 | . . . . . . 7 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V | |
5 | eqid 2771 | . . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) | |
6 | oveq1 6981 | . . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1)) | |
7 | oveq1 6981 | . . . . . . . 8 ⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1)) | |
8 | 5, 6, 7 | frsucmpt2 7877 | . . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1)) |
9 | 4, 8 | mpan2 679 | . . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1)) |
10 | peano2 7415 | . . . . . . . 8 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω) | |
11 | fnfvelrn 6671 | . . . . . . . 8 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)) | |
12 | 1, 10, 11 | sylancr 579 | . . . . . . 7 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)) |
13 | df-nn 11438 | . . . . . . . 8 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) | |
14 | df-ima 5416 | . . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) | |
15 | 13, 14 | eqtri 2795 | . . . . . . 7 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) |
16 | 12, 15 | syl6eleqr 2870 | . . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ) |
17 | 9, 16 | eqeltrrd 2860 | . . . . 5 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ) |
18 | oveq1 6981 | . . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1)) | |
19 | 18 | eleq1d 2843 | . . . . 5 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ)) |
20 | 17, 19 | syl5ibcom 237 | . . . 4 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)) |
21 | 20 | rexlimiv 3218 | . . 3 ⊢ (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ) |
22 | 3, 21 | sylbi 209 | . 2 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ) |
23 | 22, 15 | eleq2s 2877 | 1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1508 ∈ wcel 2051 ∃wrex 3082 Vcvv 3408 ↦ cmpt 5004 ran crn 5404 ↾ cres 5405 “ cima 5406 suc csuc 6028 Fn wfn 6180 ‘cfv 6185 (class class class)co 6974 ωcom 7394 reccrdg 7847 1c1 10334 + caddc 10336 ℕcn 11437 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-ral 3086 df-rex 3087 df-reu 3088 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-pss 3838 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4709 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-tr 5027 df-id 5308 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-we 5364 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-ord 6029 df-on 6030 df-lim 6031 df-suc 6032 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-ov 6977 df-om 7395 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-nn 11438 |
This theorem is referenced by: dfnn2 11452 dfnn3 11453 peano2nnd 11456 nnind 11457 nnaddcl 11461 2nn 11511 3nn 11517 4nn 11522 5nn 11526 6nn 11530 7nn 11534 8nn 11538 9nn 11542 nnunb 11701 nneo 11877 10nn 11925 fzonn0p1p1 12929 ser1const 13239 expp1 13249 facp1 13451 relexpsucnnl 14250 isercolllem1 14880 isercoll2 14884 climcndslem2 15063 climcnds 15064 harmonic 15072 trireciplem 15075 trirecip 15076 rpnnen2lem9 15433 sqrt2irr 15460 nno 15591 nnoddm1d2 15595 rplpwr 15761 prmind2 15883 eulerthlem2 15973 pcmpt 16082 pockthi 16097 prmreclem6 16111 dec5nprm 16256 mulgnnp1 18033 chfacfisf 21181 chfacfisfcpmat 21182 cayhamlem1 21193 1stcfb 21772 bcthlem3 23647 bcthlem4 23648 ovolunlem1a 23815 ovolicc2lem4 23839 voliunlem1 23869 volsup 23875 volsup2 23924 itg1climres 24033 mbfi1fseqlem5 24038 itg2monolem1 24069 itg2i1fseqle 24073 itg2i1fseq 24074 itg2i1fseq2 24075 itg2addlem 24077 itg2gt0 24079 itg2cnlem1 24080 aaliou3lem7 24656 emcllem1 25290 emcllem2 25291 emcllem3 25292 emcllem5 25294 emcllem6 25295 emcllem7 25296 zetacvg 25309 lgam1 25358 bclbnd 25573 bposlem5 25581 2sqlem10 25721 dchrisumlem2 25783 logdivbnd 25849 pntrsumo1 25858 pntrsumbnd 25859 wwlksext2clwwlk 27595 numclwwlk2lem1 27944 numclwlk2lem2f 27945 numclwlk2lem2fOLD 27948 opsqrlem5 29717 opsqrlem6 29718 nnindf 30305 psgnfzto1st 30728 esumpmono 31014 fibp1 31337 rrvsum 31390 subfacp1lem6 32054 subfaclim 32057 bcprod 32527 bccolsum 32528 iprodgam 32531 faclimlem1 32532 faclimlem2 32533 faclim2 32537 nn0prpwlem 33228 mblfinlem2 34408 volsupnfl 34415 seqpo 34501 incsequz 34502 incsequz2 34503 geomcau 34513 heiborlem6 34573 bfplem1 34579 jm2.27dlem4 39043 nnsplit 41089 sumnnodd 41376 stoweidlem20 41770 wallispilem4 41818 wallispi2lem1 41821 wallispi2lem2 41822 stirlinglem4 41827 stirlinglem8 41831 stirlinglem11 41834 stirlinglem12 41835 stirlinglem13 41836 vonioolem2 42428 vonicclem2 42431 deccarry 42951 iccpartres 42984 iccelpart 42999 odz2prm2pw 43127 fmtnoprmfac1 43129 fmtnoprmfac2 43131 lighneallem4 43177 |
Copyright terms: Public domain | W3C validator |