| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ispth 29262 |
. . 3
β’
(β
(PathsβπΊ)π β (β
(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―ββ
)))
β§ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
β
)) |
| 2 | 1 | a1i 11 |
. 2
β’ (πΊ β π β (β
(PathsβπΊ)π β (β
(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―ββ
)))
β§ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
β
))) |
| 3 | | 3anass 1094 |
. . . 4
β’
((β
(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―ββ
)))
β§ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
β
) β (β
(TrailsβπΊ)π β§ (Fun β‘(π βΎ (1..^(β―ββ
)))
β§ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
β
))) |
| 4 | 3 | a1i 11 |
. . 3
β’ (πΊ β π β ((β
(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―ββ
)))
β§ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
β
) β (β
(TrailsβπΊ)π β§ (Fun β‘(π βΎ (1..^(β―ββ
)))
β§ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
β
)))) |
| 5 | | funcnv0 6614 |
. . . . . 6
β’ Fun β‘β
|
| 6 | | hash0 14334 |
. . . . . . . . . . . 12
β’
(β―ββ
) = 0 |
| 7 | | 0le1 11744 |
. . . . . . . . . . . 12
β’ 0 β€
1 |
| 8 | 6, 7 | eqbrtri 5169 |
. . . . . . . . . . 11
β’
(β―ββ
) β€ 1 |
| 9 | | 1z 12599 |
. . . . . . . . . . . 12
β’ 1 β
β€ |
| 10 | | 0z 12576 |
. . . . . . . . . . . . 13
β’ 0 β
β€ |
| 11 | 6, 10 | eqeltri 2828 |
. . . . . . . . . . . 12
β’
(β―ββ
) β β€ |
| 12 | | fzon 13660 |
. . . . . . . . . . . 12
β’ ((1
β β€ β§ (β―ββ
) β β€) β
((β―ββ
) β€ 1 β (1..^(β―ββ
)) =
β
)) |
| 13 | 9, 11, 12 | mp2an 689 |
. . . . . . . . . . 11
β’
((β―ββ
) β€ 1 β (1..^(β―ββ
)) =
β
) |
| 14 | 8, 13 | mpbi 229 |
. . . . . . . . . 10
β’
(1..^(β―ββ
)) = β
|
| 15 | 14 | reseq2i 5978 |
. . . . . . . . 9
β’ (π βΎ
(1..^(β―ββ
))) = (π βΎ β
) |
| 16 | | res0 5985 |
. . . . . . . . 9
β’ (π βΎ β
) =
β
|
| 17 | 15, 16 | eqtri 2759 |
. . . . . . . 8
β’ (π βΎ
(1..^(β―ββ
))) = β
|
| 18 | 17 | cnveqi 5874 |
. . . . . . 7
β’ β‘(π βΎ (1..^(β―ββ
))) =
β‘β
|
| 19 | 18 | funeqi 6569 |
. . . . . 6
β’ (Fun
β‘(π βΎ (1..^(β―ββ
)))
β Fun β‘β
) |
| 20 | 5, 19 | mpbir 230 |
. . . . 5
β’ Fun β‘(π βΎ
(1..^(β―ββ
))) |
| 21 | 14 | imaeq2i 6057 |
. . . . . . . 8
β’ (π β
(1..^(β―ββ
))) = (π β β
) |
| 22 | | ima0 6076 |
. . . . . . . 8
β’ (π β β
) =
β
|
| 23 | 21, 22 | eqtri 2759 |
. . . . . . 7
β’ (π β
(1..^(β―ββ
))) = β
|
| 24 | 23 | ineq2i 4209 |
. . . . . 6
β’ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
((π β {0,
(β―ββ
)}) β© β
) |
| 25 | | in0 4391 |
. . . . . 6
β’ ((π β {0,
(β―ββ
)}) β© β
) = β
|
| 26 | 24, 25 | eqtri 2759 |
. . . . 5
β’ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
β
|
| 27 | 20, 26 | pm3.2i 470 |
. . . 4
β’ (Fun
β‘(π βΎ (1..^(β―ββ
)))
β§ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
β
) |
| 28 | 27 | biantru 529 |
. . 3
β’
(β
(TrailsβπΊ)π β (β
(TrailsβπΊ)π β§ (Fun β‘(π βΎ (1..^(β―ββ
)))
β§ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
β
))) |
| 29 | 4, 28 | bitr4di 289 |
. 2
β’ (πΊ β π β ((β
(TrailsβπΊ)π β§ Fun β‘(π βΎ (1..^(β―ββ
)))
β§ ((π β {0,
(β―ββ
)}) β© (π β (1..^(β―ββ
)))) =
β
) β β
(TrailsβπΊ)π)) |
| 30 | | 0pth.v |
. . 3
β’ π = (VtxβπΊ) |
| 31 | 30 | 0trl 29657 |
. 2
β’ (πΊ β π β (β
(TrailsβπΊ)π β π:(0...0)βΆπ)) |
| 32 | 2, 29, 31 | 3bitrd 305 |
1
β’ (πΊ β π β (β
(PathsβπΊ)π β π:(0...0)βΆπ)) |
