Step | Hyp | Ref
| Expression |
1 | | pthsfval 28975 |
. . . 4
β’
(PathsβπΊ) =
{β¨π, πβ© β£ (π(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπ))) β§ ((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) =
β
)} |
2 | | 3anass 1095 |
. . . . 5
β’ ((π(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπ))) β§ ((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) = β
) β (π(TrailsβπΊ)π β§ (Fun β‘(π βΎ (1..^(β―βπ))) β§ ((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) =
β
))) |
3 | 2 | opabbii 5215 |
. . . 4
β’
{β¨π, πβ© β£ (π(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπ))) β§ ((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) = β
)} = {β¨π, πβ© β£ (π(TrailsβπΊ)π β§ (Fun β‘(π βΎ (1..^(β―βπ))) β§ ((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) =
β
))} |
4 | 1, 3 | eqtri 2760 |
. . 3
β’
(PathsβπΊ) =
{β¨π, πβ© β£ (π(TrailsβπΊ)π β§ (Fun β‘(π βΎ (1..^(β―βπ))) β§ ((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) =
β
))} |
5 | | simpr 485 |
. . . . . . 7
β’ ((π = πΉ β§ π = π) β π = π) |
6 | | fveq2 6891 |
. . . . . . . . 9
β’ (π = πΉ β (β―βπ) = (β―βπΉ)) |
7 | 6 | oveq2d 7424 |
. . . . . . . 8
β’ (π = πΉ β (1..^(β―βπ)) = (1..^(β―βπΉ))) |
8 | 7 | adantr 481 |
. . . . . . 7
β’ ((π = πΉ β§ π = π) β (1..^(β―βπ)) = (1..^(β―βπΉ))) |
9 | 5, 8 | reseq12d 5982 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β (π βΎ (1..^(β―βπ))) = (π βΎ (1..^(β―βπΉ)))) |
10 | 9 | cnveqd 5875 |
. . . . 5
β’ ((π = πΉ β§ π = π) β β‘(π βΎ (1..^(β―βπ))) = β‘(π βΎ (1..^(β―βπΉ)))) |
11 | 10 | funeqd 6570 |
. . . 4
β’ ((π = πΉ β§ π = π) β (Fun β‘(π βΎ (1..^(β―βπ))) β Fun β‘(π βΎ (1..^(β―βπΉ))))) |
12 | 6 | preq2d 4744 |
. . . . . . . 8
β’ (π = πΉ β {0, (β―βπ)} = {0, (β―βπΉ)}) |
13 | 12 | adantr 481 |
. . . . . . 7
β’ ((π = πΉ β§ π = π) β {0, (β―βπ)} = {0, (β―βπΉ)}) |
14 | 5, 13 | imaeq12d 6060 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β (π β {0, (β―βπ)}) = (π β {0, (β―βπΉ)})) |
15 | 5, 8 | imaeq12d 6060 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β (π β (1..^(β―βπ))) = (π β (1..^(β―βπΉ)))) |
16 | 14, 15 | ineq12d 4213 |
. . . . 5
β’ ((π = πΉ β§ π = π) β ((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) = ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ))))) |
17 | 16 | eqeq1d 2734 |
. . . 4
β’ ((π = πΉ β§ π = π) β (((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) = β
β ((π β {0,
(β―βπΉ)}) β©
(π β
(1..^(β―βπΉ)))) =
β
)) |
18 | 11, 17 | anbi12d 631 |
. . 3
β’ ((π = πΉ β§ π = π) β ((Fun β‘(π βΎ (1..^(β―βπ))) β§ ((π β {0, (β―βπ)}) β© (π β (1..^(β―βπ)))) = β
) β (Fun
β‘(π βΎ (1..^(β―βπΉ))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) =
β
))) |
19 | | reltrls 28948 |
. . 3
β’ Rel
(TrailsβπΊ) |
20 | 4, 18, 19 | brfvopabrbr 6995 |
. 2
β’ (πΉ(PathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ (Fun β‘(π βΎ (1..^(β―βπΉ))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) =
β
))) |
21 | | 3anass 1095 |
. 2
β’ ((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β (πΉ(TrailsβπΊ)π β§ (Fun β‘(π βΎ (1..^(β―βπΉ))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) =
β
))) |
22 | 20, 21 | bitr4i 277 |
1
β’ (πΉ(PathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) =
β
)) |