Step | Hyp | Ref
| Expression |
1 | | fvex 6904 |
. . . . 5
β’
(Vtxβπ) β
V |
2 | 1, 1 | pm3.2i 470 |
. . . 4
β’
((Vtxβπ)
β V β§ (Vtxβπ) β V) |
3 | 2 | rgen2w 3065 |
. . 3
β’
βπ β
β0 βπ β V ((Vtxβπ) β V β§ (Vtxβπ) β V) |
4 | | df-wspthsnon 29356 |
. . . 4
β’
WSPathsNOn = (π β
β0, π
β V β¦ (π β
(Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€})) |
5 | | fveq2 6891 |
. . . . . 6
β’ (π = πΊ β (Vtxβπ) = (VtxβπΊ)) |
6 | 5, 5 | jca 511 |
. . . . 5
β’ (π = πΊ β ((Vtxβπ) = (VtxβπΊ) β§ (Vtxβπ) = (VtxβπΊ))) |
7 | 6 | adantl 481 |
. . . 4
β’ ((π = π β§ π = πΊ) β ((Vtxβπ) = (VtxβπΊ) β§ (Vtxβπ) = (VtxβπΊ))) |
8 | 4, 7 | el2mpocl 8076 |
. . 3
β’
(βπ β
β0 βπ β V ((Vtxβπ) β V β§ (Vtxβπ) β V) β (π β (π΄(π WSPathsNOn πΊ)π΅) β ((π β β0 β§ πΊ β V) β§ (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ))))) |
9 | 3, 8 | ax-mp 5 |
. 2
β’ (π β (π΄(π WSPathsNOn πΊ)π΅) β ((π β β0 β§ πΊ β V) β§ (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)))) |
10 | | simprl 768 |
. . 3
β’ ((π β (π΄(π WSPathsNOn πΊ)π΅) β§ ((π β β0 β§ πΊ β V) β§ (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)))) β (π β β0 β§ πΊ β V)) |
11 | | wspthnonp.v |
. . . . . . . 8
β’ π = (VtxβπΊ) |
12 | 11 | eleq2i 2824 |
. . . . . . 7
β’ (π΄ β π β π΄ β (VtxβπΊ)) |
13 | 11 | eleq2i 2824 |
. . . . . . 7
β’ (π΅ β π β π΅ β (VtxβπΊ)) |
14 | 12, 13 | anbi12i 626 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π) β (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ))) |
15 | 14 | biimpri 227 |
. . . . 5
β’ ((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β (π΄ β π β§ π΅ β π)) |
16 | 15 | adantl 481 |
. . . 4
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ))) β (π΄ β π β§ π΅ β π)) |
17 | 16 | adantl 481 |
. . 3
β’ ((π β (π΄(π WSPathsNOn πΊ)π΅) β§ ((π β β0 β§ πΊ β V) β§ (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)))) β (π΄ β π β§ π΅ β π)) |
18 | | wspthnon 29380 |
. . . . 5
β’ (π β (π΄(π WSPathsNOn πΊ)π΅) β (π β (π΄(π WWalksNOn πΊ)π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π)) |
19 | 18 | biimpi 215 |
. . . 4
β’ (π β (π΄(π WSPathsNOn πΊ)π΅) β (π β (π΄(π WWalksNOn πΊ)π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π)) |
20 | 19 | adantr 480 |
. . 3
β’ ((π β (π΄(π WSPathsNOn πΊ)π΅) β§ ((π β β0 β§ πΊ β V) β§ (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)))) β (π β (π΄(π WWalksNOn πΊ)π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π)) |
21 | 10, 17, 20 | 3jca 1127 |
. 2
β’ ((π β (π΄(π WSPathsNOn πΊ)π΅) β§ ((π β β0 β§ πΊ β V) β§ (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)))) β ((π β β0 β§ πΊ β V) β§ (π΄ β π β§ π΅ β π) β§ (π β (π΄(π WWalksNOn πΊ)π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π))) |
22 | 9, 21 | mpdan 684 |
1
β’ (π β (π΄(π WSPathsNOn πΊ)π΅) β ((π β β0 β§ πΊ β V) β§ (π΄ β π β§ π΅ β π) β§ (π β (π΄(π WWalksNOn πΊ)π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π))) |