Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. . . . 5
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β (π₯ prefix (π + 1)) = (π₯ prefix (π + 1))) |
2 | | wwlksnextprop.x |
. . . . . . . . 9
β’ π = ((π + 1) WWalksN πΊ) |
3 | 2 | wwlksnextproplem1 29163 |
. . . . . . . 8
β’ ((π₯ β π β§ π β β0) β ((π₯ prefix (π + 1))β0) = (π₯β0)) |
4 | 3 | ancoms 460 |
. . . . . . 7
β’ ((π β β0
β§ π₯ β π) β ((π₯ prefix (π + 1))β0) = (π₯β0)) |
5 | 4 | adantr 482 |
. . . . . 6
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β ((π₯ prefix (π + 1))β0) = (π₯β0)) |
6 | | eqeq2 2745 |
. . . . . . 7
β’ ((π₯β0) = π β (((π₯ prefix (π + 1))β0) = (π₯β0) β ((π₯ prefix (π + 1))β0) = π)) |
7 | 6 | adantl 483 |
. . . . . 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 29164 |
. . . . . . 7
β’ ((π₯ β π β§ π β β0) β
{(lastSβ(π₯ prefix
(π + 1))),
(lastSβπ₯)} β
πΈ) |
11 | 10 | ancoms 460 |
. . . . . 6
β’ ((π β β0
β§ π₯ β π) β {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)} β πΈ) |
12 | 11 | adantr 482 |
. . . . 5
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)} β πΈ) |
13 | | simpr 486 |
. . . . . . . 8
β’ ((π β β0
β§ π₯ β π) β π₯ β π) |
14 | 13 | adantr 482 |
. . . . . . 7
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β π₯ β π) |
15 | | simpr 486 |
. . . . . . 7
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β (π₯β0) = π) |
16 | | simpll 766 |
. . . . . . 7
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β π β
β0) |
17 | | wwlksnextprop.y |
. . . . . . . 8
β’ π = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} |
18 | 2, 9, 17 | wwlksnextproplem3 29165 |
. . . . . . 7
β’ ((π₯ β π β§ (π₯β0) = π β§ π β β0) β (π₯ prefix (π + 1)) β π) |
19 | 14, 15, 16, 18 | syl3anc 1372 |
. . . . . 6
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β (π₯ prefix (π + 1)) β π) |
20 | | eqeq2 2745 |
. . . . . . . 8
β’ (π¦ = (π₯ prefix (π + 1)) β ((π₯ prefix (π + 1)) = π¦ β (π₯ prefix (π + 1)) = (π₯ prefix (π + 1)))) |
21 | | fveq1 6891 |
. . . . . . . . 9
β’ (π¦ = (π₯ prefix (π + 1)) β (π¦β0) = ((π₯ prefix (π + 1))β0)) |
22 | 21 | eqeq1d 2735 |
. . . . . . . 8
β’ (π¦ = (π₯ prefix (π + 1)) β ((π¦β0) = π β ((π₯ prefix (π + 1))β0) = π)) |
23 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π¦ = (π₯ prefix (π + 1)) β (lastSβπ¦) = (lastSβ(π₯ prefix (π + 1)))) |
24 | 23 | preq1d 4744 |
. . . . . . . . 9
β’ (π¦ = (π₯ prefix (π + 1)) β {(lastSβπ¦), (lastSβπ₯)} = {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)}) |
25 | 24 | eleq1d 2819 |
. . . . . . . 8
β’ (π¦ = (π₯ prefix (π + 1)) β ({(lastSβπ¦), (lastSβπ₯)} β πΈ β {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)} β πΈ)) |
26 | 20, 22, 25 | 3anbi123d 1437 |
. . . . . . 7
β’ (π¦ = (π₯ prefix (π + 1)) β (((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ) β ((π₯ prefix (π + 1)) = (π₯ prefix (π + 1)) β§ ((π₯ prefix (π + 1))β0) = π β§ {(lastSβ(π₯ prefix (π + 1))), (lastSβπ₯)} β πΈ))) |
27 | 26 | adantl 483 |
. . . . . 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 3606 |
. . . . 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 1465 |
. . . 4
β’ (((π β β0
β§ π₯ β π) β§ (π₯β0) = π) β βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ)) |
30 | 29 | ex 414 |
. . 3
β’ ((π β β0
β§ π₯ β π) β ((π₯β0) = π β βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ))) |
31 | 21 | eqcoms 2741 |
. . . . . . . . 9
β’ ((π₯ prefix (π + 1)) = π¦ β (π¦β0) = ((π₯ prefix (π + 1))β0)) |
32 | 31 | eqeq1d 2735 |
. . . . . . . 8
β’ ((π₯ prefix (π + 1)) = π¦ β ((π¦β0) = π β ((π₯ prefix (π + 1))β0) = π)) |
33 | 3 | eqcomd 2739 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π β β0) β (π₯β0) = ((π₯ prefix (π + 1))β0)) |
34 | 33 | ancoms 460 |
. . . . . . . . . 10
β’ ((π β β0
β§ π₯ β π) β (π₯β0) = ((π₯ prefix (π + 1))β0)) |
35 | 34 | adantr 482 |
. . . . . . . . 9
β’ (((π β β0
β§ π₯ β π) β§ π¦ β π) β (π₯β0) = ((π₯ prefix (π + 1))β0)) |
36 | | eqeq2 2745 |
. . . . . . . . . 10
β’ (π = ((π₯ prefix (π + 1))β0) β ((π₯β0) = π β (π₯β0) = ((π₯ prefix (π + 1))β0))) |
37 | 36 | eqcoms 2741 |
. . . . . . . . 9
β’ (((π₯ prefix (π + 1))β0) = π β ((π₯β0) = π β (π₯β0) = ((π₯ prefix (π + 1))β0))) |
38 | 35, 37 | imbitrrid 245 |
. . . . . . . 8
β’ (((π₯ prefix (π + 1))β0) = π β (((π β β0 β§ π₯ β π) β§ π¦ β π) β (π₯β0) = π)) |
39 | 32, 38 | syl6bi 253 |
. . . . . . 7
β’ ((π₯ prefix (π + 1)) = π¦ β ((π¦β0) = π β (((π β β0 β§ π₯ β π) β§ π¦ β π) β (π₯β0) = π))) |
40 | 39 | imp 408 |
. . . . . 6
β’ (((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π) β (((π β β0 β§ π₯ β π) β§ π¦ β π) β (π₯β0) = π)) |
41 | 40 | 3adant3 1133 |
. . . . 5
β’ (((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ) β (((π β β0 β§ π₯ β π) β§ π¦ β π) β (π₯β0) = π)) |
42 | 41 | com12 32 |
. . . 4
β’ (((π β β0
β§ π₯ β π) β§ π¦ β π) β (((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ) β (π₯β0) = π)) |
43 | 42 | rexlimdva 3156 |
. . 3
β’ ((π β β0
β§ π₯ β π) β (βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ) β (π₯β0) = π)) |
44 | 30, 43 | impbid 211 |
. 2
β’ ((π β β0
β§ π₯ β π) β ((π₯β0) = π β βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ))) |
45 | 44 | rabbidva 3440 |
1
β’ (π β β0
β {π₯ β π β£ (π₯β0) = π} = {π₯ β π β£ βπ¦ β π ((π₯ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ₯)} β πΈ)}) |