| 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 8475 | . . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω | |
| 2 | fvelrnb 6969 | . . . 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 7464 | . . . . . . 7 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V | |
| 5 | eqid 2737 | . . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) | |
| 6 | oveq1 7438 | . . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1)) | |
| 7 | oveq1 7438 | . . . . . . . 8 ⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1)) | |
| 8 | 5, 6, 7 | frsucmpt2 8480 | . . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1)) |
| 9 | 4, 8 | mpan2 691 | . . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1)) |
| 10 | peano2 7912 | . . . . . . . 8 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω) | |
| 11 | fnfvelrn 7100 | . . . . . . . 8 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)) | |
| 12 | 1, 10, 11 | sylancr 587 | . . . . . . 7 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)) |
| 13 | df-nn 12267 | . . . . . . . 8 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) | |
| 14 | df-ima 5698 | . . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) | |
| 15 | 13, 14 | eqtri 2765 | . . . . . . 7 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) |
| 16 | 12, 15 | eleqtrrdi 2852 | . . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ) |
| 17 | 9, 16 | eqeltrrd 2842 | . . . . 5 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ) |
| 18 | oveq1 7438 | . . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1)) | |
| 19 | 18 | eleq1d 2826 | . . . . 5 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ)) |
| 20 | 17, 19 | syl5ibcom 245 | . . . 4 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)) |
| 21 | 20 | rexlimiv 3148 | . . 3 ⊢ (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ) |
| 22 | 3, 21 | sylbi 217 | . 2 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ) |
| 23 | 22, 15 | eleq2s 2859 | 1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 ∃wrex 3070 Vcvv 3480 ↦ cmpt 5225 ran crn 5686 ↾ cres 5687 “ cima 5688 suc csuc 6386 Fn wfn 6556 ‘cfv 6561 (class class class)co 7431 ωcom 7887 reccrdg 8449 1c1 11156 + caddc 11158 ℕcn 12266 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-om 7888 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-nn 12267 |
| This theorem is referenced by: dfnn2 12279 dfnn3 12280 peano2nnd 12283 nnind 12284 nnaddcl 12289 2nn 12339 3nn 12345 4nn 12349 5nn 12352 6nn 12355 7nn 12358 8nn 12361 9nn 12364 nnunb 12522 nneo 12702 10nn 12749 fzonn0p1p1 13783 ser1const 14099 expp1 14109 facp1 14317 relexpsucnnl 15069 isercolllem1 15701 isercoll2 15705 climcndslem2 15886 climcnds 15887 harmonic 15895 trireciplem 15898 trirecip 15899 rpnnen2lem9 16258 sqrt2irr 16285 nno 16419 nnoddm1d2 16423 rplpwr 16595 prmind2 16722 eulerthlem2 16819 pcmpt 16930 pockthi 16945 prmreclem6 16959 dec5nprm 17104 mulgnnp1 19100 chfacfisf 22860 chfacfisfcpmat 22861 cayhamlem1 22872 1stcfb 23453 bcthlem3 25360 bcthlem4 25361 ovolunlem1a 25531 ovolicc2lem4 25555 voliunlem1 25585 volsup 25591 volsup2 25640 itg1climres 25749 mbfi1fseqlem5 25754 itg2monolem1 25785 itg2i1fseqle 25789 itg2i1fseq 25790 itg2i1fseq2 25791 itg2addlem 25793 itg2gt0 25795 itg2cnlem1 25796 aaliou3lem7 26391 emcllem1 27039 emcllem2 27040 emcllem3 27041 emcllem5 27043 emcllem6 27044 emcllem7 27045 zetacvg 27058 lgam1 27107 bclbnd 27324 bposlem5 27332 2sqlem10 27472 dchrisumlem2 27534 logdivbnd 27600 pntrsumo1 27609 pntrsumbnd 27610 wwlksext2clwwlk 30076 numclwwlk2lem1 30395 numclwlk2lem2f 30396 opsqrlem5 32163 opsqrlem6 32164 nnindf 32821 psgnfzto1st 33125 esumpmono 34080 fibp1 34403 rrvsum 34456 subfacp1lem6 35190 subfaclim 35193 bcprod 35738 bccolsum 35739 iprodgam 35742 faclimlem1 35743 faclimlem2 35744 faclim2 35748 nn0prpwlem 36323 mblfinlem2 37665 volsupnfl 37672 seqpo 37754 incsequz 37755 incsequz2 37756 geomcau 37766 heiborlem6 37823 bfplem1 37829 fimgmcyc 42544 fsuppind 42600 jm2.27dlem4 43024 nnsplit 45369 sumnnodd 45645 stoweidlem20 46035 wallispilem4 46083 wallispi2lem1 46086 wallispi2lem2 46087 stirlinglem4 46092 stirlinglem8 46096 stirlinglem11 46099 stirlinglem12 46100 stirlinglem13 46101 vonioolem2 46696 vonicclem2 46699 deccarry 47323 iccpartres 47405 iccelpart 47420 odz2prm2pw 47550 fmtnoprmfac1 47552 fmtnoprmfac2 47554 lighneallem4 47597 |
| Copyright terms: Public domain | W3C validator |