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 2697 | . 2 | |
2 | simpl 108 | . . . . . 6 | |
3 | eleq1 2202 | . . . . . . . 8 | |
4 | suceq 4324 | . . . . . . . . 9 | |
5 | 4 | eleq1d 2208 | . . . . . . . 8 |
6 | 3, 5 | imbi12d 233 | . . . . . . 7 |
7 | 6 | adantl 275 | . . . . . 6 |
8 | df-clab 2126 | . . . . . . . . 9 | |
9 | simpr 109 | . . . . . . . . . . . 12 | |
10 | df-ral 2421 | . . . . . . . . . . . 12 | |
11 | 9, 10 | sylib 121 | . . . . . . . . . . 11 |
12 | 11 | sbimi 1737 | . . . . . . . . . 10 |
13 | sbim 1926 | . . . . . . . . . . . 12 | |
14 | clelsb4 2245 | . . . . . . . . . . . . 13 | |
15 | clelsb4 2245 | . . . . . . . . . . . . 13 | |
16 | 14, 15 | imbi12i 238 | . . . . . . . . . . . 12 |
17 | 13, 16 | bitri 183 | . . . . . . . . . . 11 |
18 | 17 | sbalv 1980 | . . . . . . . . . 10 |
19 | 12, 18 | sylib 121 | . . . . . . . . 9 |
20 | 8, 19 | sylbi 120 | . . . . . . . 8 |
21 | 20 | 19.21bi 1537 | . . . . . . 7 |
22 | 21 | adantl 275 | . . . . . 6 |
23 | nfv 1508 | . . . . . . 7 | |
24 | nfv 1508 | . . . . . . . . 9 | |
25 | nfra1 2466 | . . . . . . . . 9 | |
26 | 24, 25 | nfan 1544 | . . . . . . . 8 |
27 | 26 | nfsab 2131 | . . . . . . 7 |
28 | 23, 27 | nfan 1544 | . . . . . 6 |
29 | nfcvd 2282 | . . . . . 6 | |
30 | nfvd 1509 | . . . . . 6 | |
31 | 2, 7, 22, 28, 29, 30 | vtocldf 2737 | . . . . 5 |
32 | 31 | ralrimiva 2505 | . . . 4 |
33 | ralim 2491 | . . . . 5 | |
34 | elintg 3779 | . . . . . 6 | |
35 | sucexg 4414 | . . . . . . 7 | |
36 | elintg 3779 | . . . . . . 7 | |
37 | 35, 36 | syl 14 | . . . . . 6 |
38 | 34, 37 | imbi12d 233 | . . . . 5 |
39 | 33, 38 | syl5ibr 155 | . . . 4 |
40 | 32, 39 | mpd 13 | . . 3 |
41 | dfom3 4506 | . . . 4 | |
42 | 41 | eleq2i 2206 | . . 3 |
43 | 41 | eleq2i 2206 | . . 3 |
44 | 40, 42, 43 | 3imtr4g 204 | . 2 |
45 | 1, 44 | mpcom 36 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wal 1329 wceq 1331 wcel 1480 wsb 1735 cab 2125 wral 2416 cvv 2686 c0 3363 cint 3771 csuc 4287 com 4504 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-pr 4131 ax-un 4355 |
This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ral 2421 df-rex 2422 df-v 2688 df-un 3075 df-in 3077 df-ss 3084 df-pw 3512 df-sn 3533 df-pr 3534 df-uni 3737 df-int 3772 df-suc 4293 df-iom 4505 |
This theorem is referenced by: peano5 4512 limom 4527 peano2b 4528 nnregexmid 4534 omsinds 4535 freccllem 6299 frecfcllem 6301 frecsuclem 6303 frecrdg 6305 nnacl 6376 nnacom 6380 nnmsucr 6384 nnsucsssuc 6388 nnaword 6407 1onn 6416 2onn 6417 3onn 6418 4onn 6419 nnaordex 6423 php5 6752 phplem4dom 6756 php5dom 6757 phplem4on 6761 dif1en 6773 findcard 6782 findcard2 6783 findcard2s 6784 infnfi 6789 unsnfi 6807 omp1eomlem 6979 ctmlemr 6993 infnninf 7022 nnnninf 7023 frec2uzrand 10178 frecuzrdgsuc 10187 frecuzrdgsuctlem 10196 frecfzennn 10199 hashunlem 10550 ennnfonelemk 11913 ennnfonelemg 11916 ennnfonelemkh 11925 ennnfonelemhf1o 11926 ennnfonelemex 11927 ennnfonelemrn 11932 ennnfonelemnn0 11935 ctinfomlemom 11940 0nninf 13197 nnsf 13199 peano4nninf 13200 nninfalllemn 13202 nninfsellemdc 13206 nninfsellemsuc 13208 nninfself 13209 nninfsellemeqinf 13212 |
Copyright terms: Public domain | W3C validator |