Step | Hyp | Ref
| Expression |
1 | | df-wwlks 28824 |
. . 3
β’ WWalks =
(π β V β¦ {π€ β Word (Vtxβπ) β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ))}) |
2 | | fveq2 6846 |
. . . . . 6
β’ (π = πΊ β (Vtxβπ) = (VtxβπΊ)) |
3 | | wwlks.v |
. . . . . 6
β’ π = (VtxβπΊ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . 5
β’ (π = πΊ β (Vtxβπ) = π) |
5 | | wrdeq 14433 |
. . . . 5
β’
((Vtxβπ) =
π β Word
(Vtxβπ) = Word π) |
6 | 4, 5 | syl 17 |
. . . 4
β’ (π = πΊ β Word (Vtxβπ) = Word π) |
7 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΊ β (Edgβπ) = (EdgβπΊ)) |
8 | | wwlks.e |
. . . . . . . 8
β’ πΈ = (EdgβπΊ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΊ β (Edgβπ) = πΈ) |
10 | 9 | eleq2d 2820 |
. . . . . 6
β’ (π = πΊ β ({(π€βπ), (π€β(π + 1))} β (Edgβπ) β {(π€βπ), (π€β(π + 1))} β πΈ)) |
11 | 10 | ralbidv 3171 |
. . . . 5
β’ (π = πΊ β (βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ) β βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β πΈ)) |
12 | 11 | anbi2d 630 |
. . . 4
β’ (π = πΊ β ((π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ)) β (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ))) |
13 | 6, 12 | rabeqbidv 3423 |
. . 3
β’ (π = πΊ β {π€ β Word (Vtxβπ) β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ))} = {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)}) |
14 | | id 22 |
. . 3
β’ (πΊ β V β πΊ β V) |
15 | 3 | fvexi 6860 |
. . . . 5
β’ π β V |
16 | 15 | a1i 11 |
. . . 4
β’ (πΊ β V β π β V) |
17 | | wrdexg 14421 |
. . . 4
β’ (π β V β Word π β V) |
18 | | rabexg 5292 |
. . . 4
β’ (Word
π β V β {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)} β V) |
19 | 16, 17, 18 | 3syl 18 |
. . 3
β’ (πΊ β V β {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)} β V) |
20 | 1, 13, 14, 19 | fvmptd3 6975 |
. 2
β’ (πΊ β V β
(WWalksβπΊ) = {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)}) |
21 | | fvprc 6838 |
. . 3
β’ (Β¬
πΊ β V β
(WWalksβπΊ) =
β
) |
22 | | fvprc 6838 |
. . . . . . . . . 10
β’ (Β¬
πΊ β V β
(VtxβπΊ) =
β
) |
23 | 3, 22 | eqtrid 2785 |
. . . . . . . . 9
β’ (Β¬
πΊ β V β π = β
) |
24 | | wrdeq 14433 |
. . . . . . . . 9
β’ (π = β
β Word π = Word
β
) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
β’ (Β¬
πΊ β V β Word
π = Word
β
) |
26 | 25 | eleq2d 2820 |
. . . . . . 7
β’ (Β¬
πΊ β V β (π€ β Word π β π€ β Word β
)) |
27 | | 0wrd0 14437 |
. . . . . . 7
β’ (π€ β Word β
β
π€ =
β
) |
28 | 26, 27 | bitrdi 287 |
. . . . . 6
β’ (Β¬
πΊ β V β (π€ β Word π β π€ = β
)) |
29 | | nne 2944 |
. . . . . . . 8
β’ (Β¬
π€ β β
β π€ = β
) |
30 | 29 | biimpri 227 |
. . . . . . 7
β’ (π€ = β
β Β¬ π€ β β
) |
31 | 30 | intnanrd 491 |
. . . . . 6
β’ (π€ = β
β Β¬ (π€ β β
β§
βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)) |
32 | 28, 31 | syl6bi 253 |
. . . . 5
β’ (Β¬
πΊ β V β (π€ β Word π β Β¬ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ))) |
33 | 32 | ralrimiv 3139 |
. . . 4
β’ (Β¬
πΊ β V β
βπ€ β Word π Β¬ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)) |
34 | | rabeq0 4348 |
. . . 4
β’ ({π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)} = β
β βπ€ β Word π Β¬ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)) |
35 | 33, 34 | sylibr 233 |
. . 3
β’ (Β¬
πΊ β V β {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)} = β
) |
36 | 21, 35 | eqtr4d 2776 |
. 2
β’ (Β¬
πΊ β V β
(WWalksβπΊ) = {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)}) |
37 | 20, 36 | pm2.61i 182 |
1
β’
(WWalksβπΊ) =
{π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ)} |