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 2566 | . 2 | |
2 | simpl 102 | . . . . . 6 | |
3 | eleq1 2100 | . . . . . . . 8 | |
4 | suceq 4139 | . . . . . . . . 9 | |
5 | 4 | eleq1d 2106 | . . . . . . . 8 |
6 | 3, 5 | imbi12d 223 | . . . . . . 7 |
7 | 6 | adantl 262 | . . . . . 6 |
8 | df-clab 2027 | . . . . . . . . 9 | |
9 | simpr 103 | . . . . . . . . . . . 12 | |
10 | df-ral 2311 | . . . . . . . . . . . 12 | |
11 | 9, 10 | sylib 127 | . . . . . . . . . . 11 |
12 | 11 | sbimi 1647 | . . . . . . . . . 10 |
13 | sbim 1827 | . . . . . . . . . . . 12 | |
14 | elsb4 1853 | . . . . . . . . . . . . 13 | |
15 | clelsb4 2143 | . . . . . . . . . . . . 13 | |
16 | 14, 15 | imbi12i 228 | . . . . . . . . . . . 12 |
17 | 13, 16 | bitri 173 | . . . . . . . . . . 11 |
18 | 17 | sbalv 1881 | . . . . . . . . . 10 |
19 | 12, 18 | sylib 127 | . . . . . . . . 9 |
20 | 8, 19 | sylbi 114 | . . . . . . . 8 |
21 | 20 | 19.21bi 1450 | . . . . . . 7 |
22 | 21 | adantl 262 | . . . . . 6 |
23 | nfv 1421 | . . . . . . 7 | |
24 | nfv 1421 | . . . . . . . . 9 | |
25 | nfra1 2355 | . . . . . . . . 9 | |
26 | 24, 25 | nfan 1457 | . . . . . . . 8 |
27 | 26 | nfsab 2032 | . . . . . . 7 |
28 | 23, 27 | nfan 1457 | . . . . . 6 |
29 | nfcvd 2179 | . . . . . 6 | |
30 | nfvd 1422 | . . . . . 6 | |
31 | 2, 7, 22, 28, 29, 30 | vtocldf 2605 | . . . . 5 |
32 | 31 | ralrimiva 2392 | . . . 4 |
33 | ralim 2380 | . . . . 5 | |
34 | elintg 3623 | . . . . . 6 | |
35 | sucexg 4224 | . . . . . . 7 | |
36 | elintg 3623 | . . . . . . 7 | |
37 | 35, 36 | syl 14 | . . . . . 6 |
38 | 34, 37 | imbi12d 223 | . . . . 5 |
39 | 33, 38 | syl5ibr 145 | . . . 4 |
40 | 32, 39 | mpd 13 | . . 3 |
41 | dfom3 4315 | . . . 4 | |
42 | 41 | eleq2i 2104 | . . 3 |
43 | 41 | eleq2i 2104 | . . 3 |
44 | 40, 42, 43 | 3imtr4g 194 | . 2 |
45 | 1, 44 | mpcom 32 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wb 98 wal 1241 wceq 1243 wcel 1393 wsb 1645 cab 2026 wral 2306 cvv 2557 c0 3224 cint 3615 csuc 4102 com 4313 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-13 1404 ax-14 1405 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-sep 3875 ax-pow 3927 ax-pr 3944 ax-un 4170 |
This theorem depends on definitions: df-bi 110 df-3an 887 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ral 2311 df-rex 2312 df-v 2559 df-un 2922 df-in 2924 df-ss 2931 df-pw 3361 df-sn 3381 df-pr 3382 df-uni 3581 df-int 3616 df-suc 4108 df-iom 4314 |
This theorem is referenced by: peano5 4321 limom 4336 peano2b 4337 nnregexmid 4342 frecsuclem1 5987 frecsuclem3 5990 frecrdg 5992 nnacl 6059 nnacom 6063 nnmsucr 6067 nnsucsssuc 6071 nnaword 6084 1onn 6093 2onn 6094 3onn 6095 4onn 6096 nnaordex 6100 php5 6321 phplem4dom 6324 php5dom 6325 phplem4on 6329 dif1en 6337 findcard 6345 findcard2 6346 findcard2s 6347 frec2uzrand 9191 frecuzrdgsuc 9201 frecfzennn 9203 |
Copyright terms: Public domain | W3C validator |