| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > peano2 | Unicode version | ||
| Description: The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.) |
| Ref | Expression |
|---|---|
| peano2 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elex 2827 |
. 2
| |
| 2 | simpl 109 |
. . . . . 6
| |
| 3 | eleq1 2297 |
. . . . . . . 8
| |
| 4 | suceq 4525 |
. . . . . . . . 9
| |
| 5 | 4 | eleq1d 2303 |
. . . . . . . 8
|
| 6 | 3, 5 | imbi12d 234 |
. . . . . . 7
|
| 7 | 6 | adantl 277 |
. . . . . 6
|
| 8 | df-clab 2221 |
. . . . . . . . 9
| |
| 9 | simpr 110 |
. . . . . . . . . . . 12
| |
| 10 | df-ral 2527 |
. . . . . . . . . . . 12
| |
| 11 | 9, 10 | sylib 122 |
. . . . . . . . . . 11
|
| 12 | 11 | sbimi 1813 |
. . . . . . . . . 10
|
| 13 | sbim 2009 |
. . . . . . . . . . . 12
| |
| 14 | clelsb2 2340 |
. . . . . . . . . . . . 13
| |
| 15 | clelsb2 2340 |
. . . . . . . . . . . . 13
| |
| 16 | 14, 15 | imbi12i 239 |
. . . . . . . . . . . 12
|
| 17 | 13, 16 | bitri 184 |
. . . . . . . . . . 11
|
| 18 | 17 | sbalv 2061 |
. . . . . . . . . 10
|
| 19 | 12, 18 | sylib 122 |
. . . . . . . . 9
|
| 20 | 8, 19 | sylbi 121 |
. . . . . . . 8
|
| 21 | 20 | 19.21bi 1607 |
. . . . . . 7
|
| 22 | 21 | adantl 277 |
. . . . . 6
|
| 23 | nfv 1577 |
. . . . . . 7
| |
| 24 | nfv 1577 |
. . . . . . . . 9
| |
| 25 | nfra1 2575 |
. . . . . . . . 9
| |
| 26 | 24, 25 | nfan 1614 |
. . . . . . . 8
|
| 27 | 26 | nfsab 2226 |
. . . . . . 7
|
| 28 | 23, 27 | nfan 1614 |
. . . . . 6
|
| 29 | nfcvd 2387 |
. . . . . 6
| |
| 30 | nfvd 1578 |
. . . . . 6
| |
| 31 | 2, 7, 22, 28, 29, 30 | vtocldf 2868 |
. . . . 5
|
| 32 | 31 | ralrimiva 2617 |
. . . 4
|
| 33 | ralim 2603 |
. . . . 5
| |
| 34 | elintg 3959 |
. . . . . 6
| |
| 35 | sucexg 4622 |
. . . . . . 7
| |
| 36 | elintg 3959 |
. . . . . . 7
| |
| 37 | 35, 36 | syl 14 |
. . . . . 6
|
| 38 | 34, 37 | imbi12d 234 |
. . . . 5
|
| 39 | 33, 38 | imbitrrid 156 |
. . . 4
|
| 40 | 32, 39 | mpd 13 |
. . 3
|
| 41 | dfom3 4716 |
. . . 4
| |
| 42 | 41 | eleq2i 2301 |
. . 3
|
| 43 | 41 | eleq2i 2301 |
. . 3
|
| 44 | 40, 42, 43 | 3imtr4g 205 |
. 2
|
| 45 | 1, 44 | mpcom 36 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-sep 4230 ax-pow 4289 ax-pr 4324 ax-un 4556 |
| This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-nf 1510 df-sb 1812 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ral 2527 df-rex 2528 df-v 2817 df-un 3217 df-in 3219 df-ss 3226 df-pw 3673 df-sn 3697 df-pr 3698 df-uni 3917 df-int 3952 df-suc 4494 df-iom 4715 |
| This theorem is referenced by: peano5 4722 limom 4738 peano2b 4739 nnregexmid 4745 omsinds 4746 freccllem 6635 frecfcllem 6637 frecsuclem 6639 frecrdg 6641 nnacl 6715 nnacom 6719 nnmsucr 6723 nnsucsssuc 6727 nnaword 6746 1onn 6755 2onn 6756 3onn 6757 4onn 6758 nnaordex 6763 php5 7114 phplem4dom 7118 php5dom 7119 phplem4on 7124 dif1en 7138 findcard 7147 findcard2 7148 findcard2s 7149 infnfi 7154 unsnfi 7181 omp1eomlem 7387 ctmlemr 7401 nninfninc 7416 infnninf 7417 infnninfOLD 7418 nnnninf 7419 nnnninfeq 7421 nninfwlpoimlemg 7468 nninfwlpoimlemginf 7469 frec2uzrand 10771 frecuzrdgsuc 10780 frecuzrdgsuctlem 10789 frecfzennn 10792 hashunlem 11172 ennnfonelemk 13168 ennnfonelemg 13171 ennnfonelemkh 13180 ennnfonelemhf1o 13181 ennnfonelemex 13182 ennnfonelemrn 13187 ennnfonelemnn0 13190 ctinfomlemom 13195 0nninf 16799 nnsf 16800 peano4nninf 16801 nninfsellemdc 16805 nninfsellemsuc 16807 nninfself 16808 nninfsellemeqinf 16811 nnnninfex 16817 |
| Copyright terms: Public domain | W3C validator |