Step | Hyp | Ref
| Expression |
1 | | df-wspthsnon 29088 |
. . 3
β’
WSPathsNOn = (π β
β0, π
β V β¦ (π β
(Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€})) |
2 | 1 | a1i 11 |
. 2
β’ ((π β β0
β§ πΊ β π) β WSPathsNOn = (π β β0,
π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€}))) |
3 | | fveq2 6892 |
. . . . . 6
β’ (π = πΊ β (Vtxβπ) = (VtxβπΊ)) |
4 | | wwlksnon.v |
. . . . . 6
β’ π = (VtxβπΊ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . 5
β’ (π = πΊ β (Vtxβπ) = π) |
6 | 5 | adantl 483 |
. . . 4
β’ ((π = π β§ π = πΊ) β (Vtxβπ) = π) |
7 | | oveq12 7418 |
. . . . . 6
β’ ((π = π β§ π = πΊ) β (π WWalksNOn π) = (π WWalksNOn πΊ)) |
8 | 7 | oveqd 7426 |
. . . . 5
β’ ((π = π β§ π = πΊ) β (π(π WWalksNOn π)π) = (π(π WWalksNOn πΊ)π)) |
9 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = πΊ β (SPathsOnβπ) = (SPathsOnβπΊ)) |
10 | 9 | oveqd 7426 |
. . . . . . . 8
β’ (π = πΊ β (π(SPathsOnβπ)π) = (π(SPathsOnβπΊ)π)) |
11 | 10 | breqd 5160 |
. . . . . . 7
β’ (π = πΊ β (π(π(SPathsOnβπ)π)π€ β π(π(SPathsOnβπΊ)π)π€)) |
12 | 11 | adantl 483 |
. . . . . 6
β’ ((π = π β§ π = πΊ) β (π(π(SPathsOnβπ)π)π€ β π(π(SPathsOnβπΊ)π)π€)) |
13 | 12 | exbidv 1925 |
. . . . 5
β’ ((π = π β§ π = πΊ) β (βπ π(π(SPathsOnβπ)π)π€ β βπ π(π(SPathsOnβπΊ)π)π€)) |
14 | 8, 13 | rabeqbidv 3450 |
. . . 4
β’ ((π = π β§ π = πΊ) β {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€} = {π€ β (π(π WWalksNOn πΊ)π) β£ βπ π(π(SPathsOnβπΊ)π)π€}) |
15 | 6, 6, 14 | mpoeq123dv 7484 |
. . 3
β’ ((π = π β§ π = πΊ) β (π β (Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€}) = (π β π, π β π β¦ {π€ β (π(π WWalksNOn πΊ)π) β£ βπ π(π(SPathsOnβπΊ)π)π€})) |
16 | 15 | adantl 483 |
. 2
β’ (((π β β0
β§ πΊ β π) β§ (π = π β§ π = πΊ)) β (π β (Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€}) = (π β π, π β π β¦ {π€ β (π(π WWalksNOn πΊ)π) β£ βπ π(π(SPathsOnβπΊ)π)π€})) |
17 | | simpl 484 |
. 2
β’ ((π β β0
β§ πΊ β π) β π β
β0) |
18 | | elex 3493 |
. . 3
β’ (πΊ β π β πΊ β V) |
19 | 18 | adantl 483 |
. 2
β’ ((π β β0
β§ πΊ β π) β πΊ β V) |
20 | 4 | fvexi 6906 |
. . . 4
β’ π β V |
21 | 20, 20 | mpoex 8066 |
. . 3
β’ (π β π, π β π β¦ {π€ β (π(π WWalksNOn πΊ)π) β£ βπ π(π(SPathsOnβπΊ)π)π€}) β V |
22 | 21 | a1i 11 |
. 2
β’ ((π β β0
β§ πΊ β π) β (π β π, π β π β¦ {π€ β (π(π WWalksNOn πΊ)π) β£ βπ π(π(SPathsOnβπΊ)π)π€}) β V) |
23 | 2, 16, 17, 19, 22 | ovmpod 7560 |
1
β’ ((π β β0
β§ πΊ β π) β (π WSPathsNOn πΊ) = (π β π, π β π β¦ {π€ β (π(π WWalksNOn πΊ)π) β£ βπ π(π(SPathsOnβπΊ)π)π€})) |