Step | Hyp | Ref
| Expression |
1 | | trlsfval 29461 |
. 2
β’
(TrailsβπΊ) =
{β¨π, πβ© β£ (π(WalksβπΊ)π β§ Fun β‘π)} |
2 | | upgrtrls.v |
. . . . . 6
β’ π = (VtxβπΊ) |
3 | | upgrtrls.i |
. . . . . 6
β’ πΌ = (iEdgβπΊ) |
4 | 2, 3 | upgriswlk 29407 |
. . . . 5
β’ (πΊ β UPGraph β (π(WalksβπΊ)π β (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}))) |
5 | 4 | anbi1d 629 |
. . . 4
β’ (πΊ β UPGraph β ((π(WalksβπΊ)π β§ Fun β‘π) β ((π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ Fun β‘π))) |
6 | | an32 643 |
. . . . 5
β’ (((π β Word dom πΌ β§ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})) β§ Fun β‘π) β ((π β Word dom πΌ β§ Fun β‘π) β§ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}))) |
7 | | 3anass 1092 |
. . . . . 6
β’ ((π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β (π β Word dom πΌ β§ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}))) |
8 | 7 | anbi1i 623 |
. . . . 5
β’ (((π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ Fun β‘π) β ((π β Word dom πΌ β§ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})) β§ Fun β‘π)) |
9 | | 3anass 1092 |
. . . . 5
β’ (((π β Word dom πΌ β§ Fun β‘π) β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β ((π β Word dom πΌ β§ Fun β‘π) β§ (π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}))) |
10 | 6, 8, 9 | 3bitr4i 303 |
. . . 4
β’ (((π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ Fun β‘π) β ((π β Word dom πΌ β§ Fun β‘π) β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})) |
11 | 5, 10 | bitrdi 287 |
. . 3
β’ (πΊ β UPGraph β ((π(WalksβπΊ)π β§ Fun β‘π) β ((π β Word dom πΌ β§ Fun β‘π) β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}))) |
12 | 11 | opabbidv 5207 |
. 2
β’ (πΊ β UPGraph β
{β¨π, πβ© β£ (π(WalksβπΊ)π β§ Fun β‘π)} = {β¨π, πβ© β£ ((π β Word dom πΌ β§ Fun β‘π) β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})}) |
13 | 1, 12 | eqtrid 2778 |
1
β’ (πΊ β UPGraph β
(TrailsβπΊ) =
{β¨π, πβ© β£ ((π β Word dom πΌ β§ Fun β‘π) β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})}) |