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 8070 | . . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω | |
2 | fvelrnb 6726 | . . . 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 7189 | . . . . . . 7 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ V | |
5 | eqid 2821 | . . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) | |
6 | oveq1 7163 | . . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1)) | |
7 | oveq1 7163 | . . . . . . . 8 ⊢ (𝑧 = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) → (𝑧 + 1) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1)) | |
8 | 5, 6, 7 | frsucmpt2 8076 | . . . . . . 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 7602 | . . . . . . . 8 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω) | |
11 | fnfvelrn 6848 | . . . . . . . 8 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ suc 𝑦 ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)) | |
12 | 1, 10, 11 | sylancr 589 | . . . . . . 7 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)) |
13 | df-nn 11639 | . . . . . . . 8 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) | |
14 | df-ima 5568 | . . . . . . . 8 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) | |
15 | 13, 14 | eqtri 2844 | . . . . . . 7 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) |
16 | 12, 15 | eleqtrrdi 2924 | . . . . . 6 ⊢ (𝑦 ∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘suc 𝑦) ∈ ℕ) |
17 | 9, 16 | eqeltrrd 2914 | . . . . 5 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ) |
18 | oveq1 7163 | . . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) = (𝐴 + 1)) | |
19 | 18 | eleq1d 2897 | . . . . 5 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → ((((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ℕ)) |
20 | 17, 19 | syl5ibcom 247 | . . . 4 ⊢ (𝑦 ∈ ω → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ)) |
21 | 20 | rexlimiv 3280 | . . 3 ⊢ (∃𝑦 ∈ ω ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘𝑦) = 𝐴 → (𝐴 + 1) ∈ ℕ) |
22 | 3, 21 | sylbi 219 | . 2 ⊢ (𝐴 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) → (𝐴 + 1) ∈ ℕ) |
23 | 22, 15 | eleq2s 2931 | 1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1537 ∈ wcel 2114 ∃wrex 3139 Vcvv 3494 ↦ cmpt 5146 ran crn 5556 ↾ cres 5557 “ cima 5558 suc csuc 6193 Fn wfn 6350 ‘cfv 6355 (class class class)co 7156 ωcom 7580 reccrdg 8045 1c1 10538 + caddc 10540 ℕcn 11638 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-ov 7159 df-om 7581 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-nn 11639 |
This theorem is referenced by: dfnn2 11651 dfnn3 11652 peano2nnd 11655 nnind 11656 nnaddcl 11661 2nn 11711 3nn 11717 4nn 11721 5nn 11724 6nn 11727 7nn 11730 8nn 11733 9nn 11736 nnunb 11894 nneo 12067 10nn 12115 fzonn0p1p1 13117 ser1const 13427 expp1 13437 facp1 13639 relexpsucnnl 14391 isercolllem1 15021 isercoll2 15025 climcndslem2 15205 climcnds 15206 harmonic 15214 trireciplem 15217 trirecip 15218 rpnnen2lem9 15575 sqrt2irr 15602 nno 15733 nnoddm1d2 15737 rplpwr 15907 prmind2 16029 eulerthlem2 16119 pcmpt 16228 pockthi 16243 prmreclem6 16257 dec5nprm 16402 mulgnnp1 18236 chfacfisf 21462 chfacfisfcpmat 21463 cayhamlem1 21474 1stcfb 22053 bcthlem3 23929 bcthlem4 23930 ovolunlem1a 24097 ovolicc2lem4 24121 voliunlem1 24151 volsup 24157 volsup2 24206 itg1climres 24315 mbfi1fseqlem5 24320 itg2monolem1 24351 itg2i1fseqle 24355 itg2i1fseq 24356 itg2i1fseq2 24357 itg2addlem 24359 itg2gt0 24361 itg2cnlem1 24362 aaliou3lem7 24938 emcllem1 25573 emcllem2 25574 emcllem3 25575 emcllem5 25577 emcllem6 25578 emcllem7 25579 zetacvg 25592 lgam1 25641 bclbnd 25856 bposlem5 25864 2sqlem10 26004 dchrisumlem2 26066 logdivbnd 26132 pntrsumo1 26141 pntrsumbnd 26142 wwlksext2clwwlk 27836 numclwwlk2lem1 28155 numclwlk2lem2f 28156 opsqrlem5 29921 opsqrlem6 29922 nnindf 30535 psgnfzto1st 30747 esumpmono 31338 fibp1 31659 rrvsum 31712 subfacp1lem6 32432 subfaclim 32435 bcprod 32970 bccolsum 32971 iprodgam 32974 faclimlem1 32975 faclimlem2 32976 faclim2 32980 nn0prpwlem 33670 mblfinlem2 34945 volsupnfl 34952 seqpo 35037 incsequz 35038 incsequz2 35039 geomcau 35049 heiborlem6 35109 bfplem1 35115 jm2.27dlem4 39629 nnsplit 41646 sumnnodd 41931 stoweidlem20 42325 wallispilem4 42373 wallispi2lem1 42376 wallispi2lem2 42377 stirlinglem4 42382 stirlinglem8 42386 stirlinglem11 42389 stirlinglem12 42390 stirlinglem13 42391 vonioolem2 42983 vonicclem2 42986 deccarry 43531 iccpartres 43598 iccelpart 43613 odz2prm2pw 43745 fmtnoprmfac1 43747 fmtnoprmfac2 43749 lighneallem4 43795 |
Copyright terms: Public domain | W3C validator |