Step | Hyp | Ref
| Expression |
1 | | ispth 29511 |
. . . 4
β’ (πΉ(PathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) =
β
)) |
2 | | simplll 774 |
. . . . . 6
β’ ((((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ)))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β§ (πβ0) β (πβ(β―βπΉ))) β πΉ(TrailsβπΊ)π) |
3 | | trliswlk 29485 |
. . . . . . . . 9
β’ (πΉ(TrailsβπΊ)π β πΉ(WalksβπΊ)π) |
4 | | wlkcl 29403 |
. . . . . . . . 9
β’ (πΉ(WalksβπΊ)π β (β―βπΉ) β
β0) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
β’ (πΉ(TrailsβπΊ)π β (β―βπΉ) β
β0) |
6 | 5 | ad3antrrr 729 |
. . . . . . 7
β’ ((((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ)))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β§ (πβ0) β (πβ(β―βπΉ))) β (β―βπΉ) β
β0) |
7 | | eqid 2727 |
. . . . . . . . . . 11
β’
(VtxβπΊ) =
(VtxβπΊ) |
8 | 7 | wlkp 29404 |
. . . . . . . . . 10
β’ (πΉ(WalksβπΊ)π β π:(0...(β―βπΉ))βΆ(VtxβπΊ)) |
9 | 3, 8 | syl 17 |
. . . . . . . . 9
β’ (πΉ(TrailsβπΊ)π β π:(0...(β―βπΉ))βΆ(VtxβπΊ)) |
10 | 9 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ)))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β§ (πβ0) β (πβ(β―βπΉ))) β π:(0...(β―βπΉ))βΆ(VtxβπΊ)) |
11 | | simpllr 775 |
. . . . . . . 8
β’ ((((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ)))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β§ (πβ0) β (πβ(β―βπΉ))) β Fun β‘(π βΎ (1..^(β―βπΉ)))) |
12 | | simpr 484 |
. . . . . . . 8
β’ ((((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ)))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β§ (πβ0) β (πβ(β―βπΉ))) β (πβ0) β (πβ(β―βπΉ))) |
13 | 10, 11, 12 | 3jca 1126 |
. . . . . . 7
β’ ((((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ)))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β§ (πβ0) β (πβ(β―βπΉ))) β (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ Fun β‘(π βΎ (1..^(β―βπΉ))) β§ (πβ0) β (πβ(β―βπΉ)))) |
14 | | simplr 768 |
. . . . . . 7
β’ ((((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ)))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β§ (πβ0) β (πβ(β―βπΉ))) β ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) |
15 | | injresinj 13771 |
. . . . . . 7
β’
((β―βπΉ)
β β0 β ((π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ Fun β‘(π βΎ (1..^(β―βπΉ))) β§ (πβ0) β (πβ(β―βπΉ))) β (((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
β Fun β‘π))) |
16 | 6, 13, 14, 15 | syl3c 66 |
. . . . . 6
β’ ((((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ)))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β§ (πβ0) β (πβ(β―βπΉ))) β Fun β‘π) |
17 | 2, 16 | jca 511 |
. . . . 5
β’ ((((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ)))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β§ (πβ0) β (πβ(β―βπΉ))) β (πΉ(TrailsβπΊ)π β§ Fun β‘π)) |
18 | 17 | ex3 1344 |
. . . 4
β’ ((πΉ(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―βπΉ))) β§ ((π β {0, (β―βπΉ)}) β© (π β (1..^(β―βπΉ)))) = β
) β ((πβ0) β (πβ(β―βπΉ)) β (πΉ(TrailsβπΊ)π β§ Fun β‘π))) |
19 | 1, 18 | sylbi 216 |
. . 3
β’ (πΉ(PathsβπΊ)π β ((πβ0) β (πβ(β―βπΉ)) β (πΉ(TrailsβπΊ)π β§ Fun β‘π))) |
20 | 19 | imp 406 |
. 2
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) β (πβ(β―βπΉ))) β (πΉ(TrailsβπΊ)π β§ Fun β‘π)) |
21 | | isspth 29512 |
. 2
β’ (πΉ(SPathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ Fun β‘π)) |
22 | 20, 21 | sylibr 233 |
1
β’ ((πΉ(PathsβπΊ)π β§ (πβ0) β (πβ(β―βπΉ))) β πΉ(SPathsβπΊ)π) |