![]() |
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 8455 | . . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω | |
2 | fvelrnb 6953 | . . . 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 7447 | . . . . . . 7 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V | |
5 | eqid 2726 | . . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) | |
6 | oveq1 7421 | . . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1)) | |
7 | oveq1 7421 | . . . . . . . 8 ⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1)) | |
8 | 5, 6, 7 | frsucmpt2 8460 | . . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1)) |
9 | 4, 8 | mpan2 689 | . . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1)) |
10 | peano2 7892 | . . . . . . . 8 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω) | |
11 | fnfvelrn 7084 | . . . . . . . 8 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)) | |
12 | 1, 10, 11 | sylancr 585 | . . . . . . 7 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)) |
13 | df-nn 12257 | . . . . . . . 8 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) | |
14 | df-ima 5686 | . . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) | |
15 | 13, 14 | eqtri 2754 | . . . . . . 7 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) |
16 | 12, 15 | eleqtrrdi 2837 | . . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ) |
17 | 9, 16 | eqeltrrd 2827 | . . . . 5 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ) |
18 | oveq1 7421 | . . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1)) | |
19 | 18 | eleq1d 2811 | . . . . 5 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ)) |
20 | 17, 19 | syl5ibcom 244 | . . . 4 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)) |
21 | 20 | rexlimiv 3138 | . . 3 ⊢ (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ) |
22 | 3, 21 | sylbi 216 | . 2 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ) |
23 | 22, 15 | eleq2s 2844 | 1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 ∃wrex 3060 Vcvv 3463 ↦ cmpt 5227 ran crn 5674 ↾ cres 5675 “ cima 5676 suc csuc 6368 Fn wfn 6539 ‘cfv 6544 (class class class)co 7414 ωcom 7866 reccrdg 8429 1c1 11148 + caddc 11150 ℕcn 12256 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5295 ax-nul 5302 ax-pr 5424 ax-un 7736 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-reu 3366 df-rab 3421 df-v 3465 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4324 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4907 df-iun 4996 df-br 5145 df-opab 5207 df-mpt 5228 df-tr 5262 df-id 5571 df-eprel 5577 df-po 5585 df-so 5586 df-fr 5628 df-we 5630 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-pred 6303 df-ord 6369 df-on 6370 df-lim 6371 df-suc 6372 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-ov 7417 df-om 7867 df-2nd 7994 df-frecs 8286 df-wrecs 8317 df-recs 8391 df-rdg 8430 df-nn 12257 |
This theorem is referenced by: dfnn2 12269 dfnn3 12270 peano2nnd 12273 nnind 12274 nnaddcl 12279 2nn 12329 3nn 12335 4nn 12339 5nn 12342 6nn 12345 7nn 12348 8nn 12351 9nn 12354 nnunb 12512 nneo 12690 10nn 12737 fzonn0p1p1 13757 ser1const 14070 expp1 14080 facp1 14288 relexpsucnnl 15028 isercolllem1 15662 isercoll2 15666 climcndslem2 15847 climcnds 15848 harmonic 15856 trireciplem 15859 trirecip 15860 rpnnen2lem9 16217 sqrt2irr 16244 nno 16377 nnoddm1d2 16381 rplpwr 16552 prmind2 16679 eulerthlem2 16777 pcmpt 16887 pockthi 16902 prmreclem6 16916 dec5nprm 17061 mulgnnp1 19070 chfacfisf 22842 chfacfisfcpmat 22843 cayhamlem1 22854 1stcfb 23435 bcthlem3 25340 bcthlem4 25341 ovolunlem1a 25511 ovolicc2lem4 25535 voliunlem1 25565 volsup 25571 volsup2 25620 itg1climres 25730 mbfi1fseqlem5 25735 itg2monolem1 25766 itg2i1fseqle 25770 itg2i1fseq 25771 itg2i1fseq2 25772 itg2addlem 25774 itg2gt0 25776 itg2cnlem1 25777 aaliou3lem7 26372 emcllem1 27019 emcllem2 27020 emcllem3 27021 emcllem5 27023 emcllem6 27024 emcllem7 27025 zetacvg 27038 lgam1 27087 bclbnd 27304 bposlem5 27312 2sqlem10 27452 dchrisumlem2 27514 logdivbnd 27580 pntrsumo1 27589 pntrsumbnd 27590 wwlksext2clwwlk 29985 numclwwlk2lem1 30304 numclwlk2lem2f 30305 opsqrlem5 32072 opsqrlem6 32073 nnindf 32721 psgnfzto1st 32985 esumpmono 33923 fibp1 34246 rrvsum 34299 subfacp1lem6 35024 subfaclim 35027 bcprod 35571 bccolsum 35572 iprodgam 35575 faclimlem1 35576 faclimlem2 35577 faclim2 35581 nn0prpwlem 36045 mblfinlem2 37370 volsupnfl 37377 seqpo 37459 incsequz 37460 incsequz2 37461 geomcau 37471 heiborlem6 37528 bfplem1 37534 fimgmcyc 42222 fsuppind 42278 jm2.27dlem4 42705 nnsplit 45007 sumnnodd 45285 stoweidlem20 45675 wallispilem4 45723 wallispi2lem1 45726 wallispi2lem2 45727 stirlinglem4 45732 stirlinglem8 45736 stirlinglem11 45739 stirlinglem12 45740 stirlinglem13 45741 vonioolem2 46336 vonicclem2 46339 deccarry 46958 iccpartres 47024 iccelpart 47039 odz2prm2pw 47169 fmtnoprmfac1 47171 fmtnoprmfac2 47173 lighneallem4 47216 |
Copyright terms: Public domain | W3C validator |