Step | Hyp | Ref
| Expression |
1 | | peano2 7881 |
. . . . 5
β’ (π β Ο β suc π β
Ο) |
2 | | df-goal 34333 |
. . . . . 6
β’
βπππ = β¨2o, β¨π, πβ©β© |
3 | | opex 5465 |
. . . . . 6
β’
β¨2o, β¨π, πβ©β© β V |
4 | 2, 3 | eqeltri 2830 |
. . . . 5
β’
βπππ β V |
5 | | isfmlasuc 34379 |
. . . . 5
β’ ((suc
π β Ο β§
βπππ β V) β
(βπππ β (Fmlaβsuc suc π) β (βπππ β (Fmlaβsuc π) β¨ βπ’ β (Fmlaβsuc π)(βπ£ β (Fmlaβsuc π)βπππ = (π’βΌππ£) β¨ βπ β Ο
βπππ = βπππ’)))) |
6 | 1, 4, 5 | sylancl 587 |
. . . 4
β’ (π β Ο β
(βπππ β (Fmlaβsuc suc π) β (βπππ β (Fmlaβsuc π) β¨ βπ’ β (Fmlaβsuc π)(βπ£ β (Fmlaβsuc π)βπππ = (π’βΌππ£) β¨ βπ β Ο
βπππ = βπππ’)))) |
7 | 6 | adantr 482 |
. . 3
β’ ((π β Ο β§
(βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc π))) β
(βπππ β (Fmlaβsuc suc π) β (βπππ β (Fmlaβsuc π) β¨ βπ’ β (Fmlaβsuc π)(βπ£ β (Fmlaβsuc π)βπππ = (π’βΌππ£) β¨ βπ β Ο
βπππ = βπππ’)))) |
8 | | fmlasssuc 34380 |
. . . . . . . . . 10
β’ (suc
π β Ο β
(Fmlaβsuc π) β
(Fmlaβsuc suc π)) |
9 | 1, 8 | syl 17 |
. . . . . . . . 9
β’ (π β Ο β
(Fmlaβsuc π) β
(Fmlaβsuc suc π)) |
10 | 9 | sseld 3982 |
. . . . . . . 8
β’ (π β Ο β (π β (Fmlaβsuc π) β π β (Fmlaβsuc suc π))) |
11 | 10 | com12 32 |
. . . . . . 7
β’ (π β (Fmlaβsuc π) β (π β Ο β π β (Fmlaβsuc suc π))) |
12 | 11 | imim2i 16 |
. . . . . 6
β’
((βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc π)) β (βπππ β (Fmlaβsuc π) β (π β Ο β π β (Fmlaβsuc suc π)))) |
13 | 12 | com23 86 |
. . . . 5
β’
((βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc π)) β (π β Ο β
(βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc suc π)))) |
14 | 13 | impcom 409 |
. . . 4
β’ ((π β Ο β§
(βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc π))) β
(βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc suc π))) |
15 | | gonanegoal 34343 |
. . . . . . . . . . 11
β’ (π’βΌππ£) β
βπππ |
16 | | eqneqall 2952 |
. . . . . . . . . . 11
β’ ((π’βΌππ£) =
βπππ β ((π’βΌππ£) β βπππ β π β (Fmlaβsuc suc π))) |
17 | 15, 16 | mpi 20 |
. . . . . . . . . 10
β’ ((π’βΌππ£) =
βπππ β π β (Fmlaβsuc suc π)) |
18 | 17 | eqcoms 2741 |
. . . . . . . . 9
β’
(βπππ = (π’βΌππ£) β π β (Fmlaβsuc suc π)) |
19 | 18 | a1i 11 |
. . . . . . . 8
β’ (((π β Ο β§ π’ β (Fmlaβsuc π)) β§ π£ β (Fmlaβsuc π)) β (βπππ = (π’βΌππ£) β π β (Fmlaβsuc suc π))) |
20 | 19 | rexlimdva 3156 |
. . . . . . 7
β’ ((π β Ο β§ π’ β (Fmlaβsuc π)) β (βπ£ β (Fmlaβsuc π)βπππ = (π’βΌππ£) β π β (Fmlaβsuc suc π))) |
21 | | df-goal 34333 |
. . . . . . . . . . . . 13
β’
βπππ’ = β¨2o, β¨π, π’β©β© |
22 | 2, 21 | eqeq12i 2751 |
. . . . . . . . . . . 12
β’
(βπππ = βπππ’ β β¨2o, β¨π, πβ©β© = β¨2o,
β¨π, π’β©β©) |
23 | | 2oex 8477 |
. . . . . . . . . . . . 13
β’
2o β V |
24 | | opex 5465 |
. . . . . . . . . . . . 13
β’
β¨π, πβ© β V |
25 | 23, 24 | opth 5477 |
. . . . . . . . . . . 12
β’
(β¨2o, β¨π, πβ©β© = β¨2o,
β¨π, π’β©β© β (2o =
2o β§ β¨π, πβ© = β¨π, π’β©)) |
26 | 22, 25 | bitri 275 |
. . . . . . . . . . 11
β’
(βπππ = βπππ’ β (2o = 2o β§
β¨π, πβ© = β¨π, π’β©)) |
27 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π β V |
28 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π β V |
29 | 27, 28 | opth 5477 |
. . . . . . . . . . . 12
β’
(β¨π, πβ© = β¨π, π’β© β (π = π β§ π = π’)) |
30 | | eleq1w 2817 |
. . . . . . . . . . . . . . 15
β’ (π’ = π β (π’ β (Fmlaβsuc π) β π β (Fmlaβsuc π))) |
31 | 30 | eqcoms 2741 |
. . . . . . . . . . . . . 14
β’ (π = π’ β (π’ β (Fmlaβsuc π) β π β (Fmlaβsuc π))) |
32 | 31, 11 | syl6bi 253 |
. . . . . . . . . . . . 13
β’ (π = π’ β (π’ β (Fmlaβsuc π) β (π β Ο β π β (Fmlaβsuc suc π)))) |
33 | 32 | impcomd 413 |
. . . . . . . . . . . 12
β’ (π = π’ β ((π β Ο β§ π’ β (Fmlaβsuc π)) β π β (Fmlaβsuc suc π))) |
34 | 29, 33 | simplbiim 506 |
. . . . . . . . . . 11
β’
(β¨π, πβ© = β¨π, π’β© β ((π β Ο β§ π’ β (Fmlaβsuc π)) β π β (Fmlaβsuc suc π))) |
35 | 26, 34 | simplbiim 506 |
. . . . . . . . . 10
β’
(βπππ = βπππ’ β ((π β Ο β§ π’ β (Fmlaβsuc π)) β π β (Fmlaβsuc suc π))) |
36 | 35 | com12 32 |
. . . . . . . . 9
β’ ((π β Ο β§ π’ β (Fmlaβsuc π)) β
(βπππ = βπππ’ β π β (Fmlaβsuc suc π))) |
37 | 36 | adantr 482 |
. . . . . . . 8
β’ (((π β Ο β§ π’ β (Fmlaβsuc π)) β§ π β Ο) β
(βπππ = βπππ’ β π β (Fmlaβsuc suc π))) |
38 | 37 | rexlimdva 3156 |
. . . . . . 7
β’ ((π β Ο β§ π’ β (Fmlaβsuc π)) β (βπ β Ο
βπππ = βπππ’ β π β (Fmlaβsuc suc π))) |
39 | 20, 38 | jaod 858 |
. . . . . 6
β’ ((π β Ο β§ π’ β (Fmlaβsuc π)) β ((βπ£ β (Fmlaβsuc π)βπππ = (π’βΌππ£) β¨ βπ β Ο
βπππ = βπππ’) β π β (Fmlaβsuc suc π))) |
40 | 39 | rexlimdva 3156 |
. . . . 5
β’ (π β Ο β
(βπ’ β
(Fmlaβsuc π)(βπ£ β (Fmlaβsuc π)βπππ = (π’βΌππ£) β¨ βπ β Ο
βπππ = βπππ’) β π β (Fmlaβsuc suc π))) |
41 | 40 | adantr 482 |
. . . 4
β’ ((π β Ο β§
(βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc π))) β (βπ’ β (Fmlaβsuc π)(βπ£ β (Fmlaβsuc π)βπππ = (π’βΌππ£) β¨ βπ β Ο
βπππ = βπππ’) β π β (Fmlaβsuc suc π))) |
42 | 14, 41 | jaod 858 |
. . 3
β’ ((π β Ο β§
(βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc π))) β
((βπππ β (Fmlaβsuc π) β¨ βπ’ β (Fmlaβsuc π)(βπ£ β (Fmlaβsuc π)βπππ = (π’βΌππ£) β¨ βπ β Ο
βπππ = βπππ’)) β π β (Fmlaβsuc suc π))) |
43 | 7, 42 | sylbid 239 |
. 2
β’ ((π β Ο β§
(βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc π))) β
(βπππ β (Fmlaβsuc suc π) β π β (Fmlaβsuc suc π))) |
44 | 43 | ex 414 |
1
β’ (π β Ο β
((βπππ β (Fmlaβsuc π) β π β (Fmlaβsuc π)) β (βπππ β (Fmlaβsuc suc π) β π β (Fmlaβsuc suc π)))) |