Step | Hyp | Ref
| Expression |
1 | | df-upwlks 46122 |
. 2
β’ UPWalks =
(π β V β¦
{β¨π, πβ© β£ (π β Word dom
(iEdgβπ) β§ π:(0...(β―βπ))βΆ(Vtxβπ) β§ βπ β
(0..^(β―βπ))((iEdgβπ)β(πβπ)) = {(πβπ), (πβ(π + 1))})}) |
2 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΊ β (iEdgβπ) = (iEdgβπΊ)) |
3 | | upwlksfval.i |
. . . . . . . 8
β’ πΌ = (iEdgβπΊ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΊ β (iEdgβπ) = πΌ) |
5 | 4 | dmeqd 5862 |
. . . . . 6
β’ (π = πΊ β dom (iEdgβπ) = dom πΌ) |
6 | | wrdeq 14430 |
. . . . . 6
β’ (dom
(iEdgβπ) = dom πΌ β Word dom
(iEdgβπ) = Word dom
πΌ) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ (π = πΊ β Word dom (iEdgβπ) = Word dom πΌ) |
8 | 7 | eleq2d 2820 |
. . . 4
β’ (π = πΊ β (π β Word dom (iEdgβπ) β π β Word dom πΌ)) |
9 | | fveq2 6843 |
. . . . . 6
β’ (π = πΊ β (Vtxβπ) = (VtxβπΊ)) |
10 | | upwlksfval.v |
. . . . . 6
β’ π = (VtxβπΊ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . 5
β’ (π = πΊ β (Vtxβπ) = π) |
12 | 11 | feq3d 6656 |
. . . 4
β’ (π = πΊ β (π:(0...(β―βπ))βΆ(Vtxβπ) β π:(0...(β―βπ))βΆπ)) |
13 | 4 | fveq1d 6845 |
. . . . . 6
β’ (π = πΊ β ((iEdgβπ)β(πβπ)) = (πΌβ(πβπ))) |
14 | 13 | eqeq1d 2735 |
. . . . 5
β’ (π = πΊ β (((iEdgβπ)β(πβπ)) = {(πβπ), (πβ(π + 1))} β (πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})) |
15 | 14 | ralbidv 3171 |
. . . 4
β’ (π = πΊ β (βπ β (0..^(β―βπ))((iEdgβπ)β(πβπ)) = {(πβπ), (πβ(π + 1))} β βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})) |
16 | 8, 12, 15 | 3anbi123d 1437 |
. . 3
β’ (π = πΊ β ((π β Word dom (iEdgβπ) β§ π:(0...(β―βπ))βΆ(Vtxβπ) β§ βπ β (0..^(β―βπ))((iEdgβπ)β(πβπ)) = {(πβπ), (πβ(π + 1))}) β (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}))) |
17 | 16 | opabbidv 5172 |
. 2
β’ (π = πΊ β {β¨π, πβ© β£ (π β Word dom (iEdgβπ) β§ π:(0...(β―βπ))βΆ(Vtxβπ) β§ βπ β (0..^(β―βπ))((iEdgβπ)β(πβπ)) = {(πβπ), (πβ(π + 1))})} = {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})}) |
18 | | elex 3462 |
. 2
β’ (πΊ β π β πΊ β V) |
19 | | 3anass 1096 |
. . . 4
β’ ((π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β (π β Word dom πΌ β§ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}))) |
20 | 19 | opabbii 5173 |
. . 3
β’
{β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})} = {β¨π, πβ© β£ (π β Word dom πΌ β§ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}))} |
21 | 3 | fvexi 6857 |
. . . . . 6
β’ πΌ β V |
22 | 21 | dmex 7849 |
. . . . 5
β’ dom πΌ β V |
23 | | wrdexg 14418 |
. . . . 5
β’ (dom
πΌ β V β Word dom
πΌ β
V) |
24 | 22, 23 | mp1i 13 |
. . . 4
β’ (πΊ β π β Word dom πΌ β V) |
25 | | ovex 7391 |
. . . . . 6
β’
(0...(β―βπ)) β V |
26 | 10 | fvexi 6857 |
. . . . . . 7
β’ π β V |
27 | 26 | a1i 11 |
. . . . . 6
β’ ((πΊ β π β§ π β Word dom πΌ) β π β V) |
28 | | mapex 8774 |
. . . . . 6
β’
(((0...(β―βπ)) β V β§ π β V) β {π β£ π:(0...(β―βπ))βΆπ} β V) |
29 | 25, 27, 28 | sylancr 588 |
. . . . 5
β’ ((πΊ β π β§ π β Word dom πΌ) β {π β£ π:(0...(β―βπ))βΆπ} β V) |
30 | | simpl 484 |
. . . . . . 7
β’ ((π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β π:(0...(β―βπ))βΆπ) |
31 | 30 | ss2abi 4024 |
. . . . . 6
β’ {π β£ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})} β {π β£ π:(0...(β―βπ))βΆπ} |
32 | 31 | a1i 11 |
. . . . 5
β’ ((πΊ β π β§ π β Word dom πΌ) β {π β£ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})} β {π β£ π:(0...(β―βπ))βΆπ}) |
33 | 29, 32 | ssexd 5282 |
. . . 4
β’ ((πΊ β π β§ π β Word dom πΌ) β {π β£ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})} β V) |
34 | 24, 33 | opabex3d 7899 |
. . 3
β’ (πΊ β π β {β¨π, πβ© β£ (π β Word dom πΌ β§ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}))} β V) |
35 | 20, 34 | eqeltrid 2838 |
. 2
β’ (πΊ β π β {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})} β V) |
36 | 1, 17, 18, 35 | fvmptd3 6972 |
1
β’ (πΊ β π β (UPWalksβπΊ) = {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})}) |