Step | Hyp | Ref
| Expression |
1 | | eqidd 2737 |
. . . . 5
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β (π₯ prefix (π + 1)) = (π₯ prefix (π + 1))) |
2 | | wwlksnextprop.x |
. . . . . . . . 9
β’ π = ((π + 1) WWalksN πΊ) |
3 | 2 | wwlksnextproplem1 28854 |
. . . . . . . 8
β’ ((π₯ β π β§ π β β0) β ((π₯ prefix (π + 1))β0) = (π₯β0)) |
4 | 3 | ancoms 459 |
. . . . . . 7
β’ ((π β β0
β§ π₯ β π) β ((π₯ prefix (π + 1))β0) = (π₯β0)) |
5 | 4 | adantr 481 |
. . . . . 6
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β ((π₯ prefix (π + 1))β0) = (π₯β0)) |
6 | | eqeq2 2748 |
. . . . . . 7
β’ ((π₯β0) = π β (((π₯ prefix (π + 1))β0) = (π₯β0) β ((π₯ prefix (π + 1))β0) = π)) |
7 | 6 | adantl 482 |
. . . . . 6
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β (((π₯ prefix (π + 1))β0) = (π₯β0) β ((π₯ prefix (π + 1))β0) = π)) |
8 | 5, 7 | mpbid 231 |
. . . . 5
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β ((π₯ prefix (π + 1))β0) = π) |
9 | | wwlksnextprop.e |
. . . . . . . 8
β’ πΈ = (EdgβπΊ) |
10 | 2, 9 | wwlksnextproplem2 28855 |
. . . . . . 7
β’ ((π₯ β π β§ π β β0) β
{(lastSβ(π₯ prefix
(π + 1))),
(lastSβπ₯)} β
πΈ) |
11 | 10 | ancoms 459 |
. . . . . 6
β’ ((π β β0
β§ π₯ β π) β {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)} β πΈ) |
12 | 11 | adantr 481 |
. . . . 5
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)} β πΈ) |
13 | | simpr 485 |
. . . . . . . 8
β’ ((π β β0
β§ π₯ β π) β π₯ β π) |
14 | 13 | adantr 481 |
. . . . . . 7
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β π₯ β π) |
15 | | simpr 485 |
. . . . . . 7
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β (π₯β0) = π) |
16 | | simpll 765 |
. . . . . . 7
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β π β
β0) |
17 | | wwlksnextprop.y |
. . . . . . . 8
β’ π = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} |
18 | 2, 9, 17 | wwlksnextproplem3 28856 |
. . . . . . 7
β’ ((π₯ β π β§ (π₯β0) = π β§ π β β0) β (π₯ prefix (π + 1)) β π) |
19 | 14, 15, 16, 18 | syl3anc 1371 |
. . . . . 6
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β (π₯ prefix (π + 1)) β π) |
20 | | eqeq2 2748 |
. . . . . . . 8
β’ (π¦ = (π₯ prefix (π + 1)) β ((π₯ prefix (π + 1)) = π¦ β (π₯ prefix (π + 1)) = (π₯ prefix (π + 1)))) |
21 | | fveq1 6841 |
. . . . . . . . 9
β’ (π¦ = (π₯ prefix (π + 1)) β (π¦β0) = ((π₯ prefix (π + 1))β0)) |
22 | 21 | eqeq1d 2738 |
. . . . . . . 8
β’ (π¦ = (π₯ prefix (π + 1)) β ((π¦β0) = π β ((π₯ prefix (π + 1))β0) = π)) |
23 | | fveq2 6842 |
. . . . . . . . . 10
β’ (π¦ = (π₯ prefix (π + 1)) β (lastSβπ¦) = (lastSβ(π₯ prefix (π + 1)))) |
24 | 23 | preq1d 4700 |
. . . . . . . . 9
β’ (π¦ = (π₯ prefix (π + 1)) β {(lastSβπ¦), (lastSβπ₯)} = {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)}) |
25 | 24 | eleq1d 2822 |
. . . . . . . 8
β’ (π¦ = (π₯ prefix (π + 1)) β ({(lastSβπ¦), (lastSβπ₯)} β πΈ β {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)} β πΈ)) |
26 | 20, 22, 25 | 3anbi123d 1436 |
. . . . . . 7
β’ (π¦ = (π₯ prefix (π + 1)) β (((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ) β ((π₯ prefix (π + 1)) = (π₯ prefix (π + 1)) β§ ((π₯ prefix (π + 1))β0) = π β§ {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)} β πΈ))) |
27 | 26 | adantl 482 |
. . . . . 6
β’ ((((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β§ π¦ = (π₯ prefix (π + 1))) β (((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ) β ((π₯ prefix (π + 1)) = (π₯ prefix (π + 1)) β§ ((π₯ prefix (π + 1))β0) = π β§ {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)} β πΈ))) |
28 | 19, 27 | rspcedv 3574 |
. . . . 5
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β (((π₯ prefix (π + 1)) = (π₯ prefix (π + 1)) β§ ((π₯ prefix (π + 1))β0) = π β§ {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)} β πΈ) β βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ))) |
29 | 1, 8, 12, 28 | mp3and 1464 |
. . . 4
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ)) |
30 | 29 | ex 413 |
. . 3
β’ ((π β β0
β§ π₯ β π) β ((π₯β0) = π β βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ))) |
31 | 21 | eqcoms 2744 |
. . . . . . . . 9
β’ ((π₯ prefix (π + 1)) = π¦ β (π¦β0) = ((π₯ prefix (π + 1))β0)) |
32 | 31 | eqeq1d 2738 |
. . . . . . . 8
β’ ((π₯ prefix (π + 1)) = π¦ β ((π¦β0) = π β ((π₯ prefix (π + 1))β0) = π)) |
33 | 3 | eqcomd 2742 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π β β0) β (π₯β0) = ((π₯ prefix (π + 1))β0)) |
34 | 33 | ancoms 459 |
. . . . . . . . . 10
β’ ((π β β0
β§ π₯ β π) β (π₯β0) = ((π₯ prefix (π + 1))β0)) |
35 | 34 | adantr 481 |
. . . . . . . . 9
β’ (((π β β0
β§ π₯ β π) β§ π¦ β π) β (π₯β0) = ((π₯ prefix (π + 1))β0)) |
36 | | eqeq2 2748 |
. . . . . . . . . 10
β’ (π = ((π₯ prefix (π + 1))β0) β ((π₯β0) = π β (π₯β0) = ((π₯ prefix (π + 1))β0))) |
37 | 36 | eqcoms 2744 |
. . . . . . . . 9
β’ (((π₯ prefix (π + 1))β0) = π β ((π₯β0) = π β (π₯β0) = ((π₯ prefix (π + 1))β0))) |
38 | 35, 37 | syl5ibr 245 |
. . . . . . . 8
β’ (((π₯ prefix (π + 1))β0) = π β (((π β β0 β§ π₯ β π) β§ π¦ β π) β (π₯β0) = π)) |
39 | 32, 38 | syl6bi 252 |
. . . . . . 7
β’ ((π₯ prefix (π + 1)) = π¦ β ((π¦β0) = π β (((π β β0 β§ π₯ β π) β§ π¦ β π) β (π₯β0) = π))) |
40 | 39 | imp 407 |
. . . . . 6
β’ (((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π) β (((π β β0 β§ π₯ β π) β§ π¦ β π) β (π₯β0) = π)) |
41 | 40 | 3adant3 1132 |
. . . . 5
β’ (((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ) β (((π β β0 β§ π₯ β π) β§ π¦ β π) β (π₯β0) = π)) |
42 | 41 | com12 32 |
. . . 4
β’ (((π β β0
β§ π₯ β π) β§ π¦ β π) β (((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ) β (π₯β0) = π)) |
43 | 42 | rexlimdva 3152 |
. . 3
β’ ((π β β0
β§ π₯ β π) β (βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ) β (π₯β0) = π)) |
44 | 30, 43 | impbid 211 |
. 2
β’ ((π β β0
β§ π₯ β π) β ((π₯β0) = π β βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ))) |
45 | 44 | rabbidva 3414 |
1
β’ (π β β0
β {π₯ β π β£ (π₯β0) = π} = {π₯ β π β£ βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ)}) |