Step | Hyp | Ref
| Expression |
1 | | df-conngr 29440 |
. . 3
β’ ConnGraph
= {π β£
[(Vtxβπ) /
π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π} |
2 | 1 | eleq2i 2826 |
. 2
β’ (πΊ β ConnGraph β πΊ β {π β£ [(Vtxβπ) / π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π}) |
3 | | fvex 6905 |
. . . . . 6
β’
(Vtxβπ) β
V |
4 | | raleq 3323 |
. . . . . . 7
β’ (π£ = (Vtxβπ) β (βπ β π£ βπβπ π(π(PathsOnβπ)π)π β βπ β (Vtxβπ)βπβπ π(π(PathsOnβπ)π)π)) |
5 | 4 | raleqbi1dv 3334 |
. . . . . 6
β’ (π£ = (Vtxβπ) β (βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π β βπ β (Vtxβπ)βπ β (Vtxβπ)βπβπ π(π(PathsOnβπ)π)π)) |
6 | 3, 5 | sbcie 3821 |
. . . . 5
β’
([(Vtxβπ) / π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π β βπ β (Vtxβπ)βπ β (Vtxβπ)βπβπ π(π(PathsOnβπ)π)π) |
7 | 6 | abbii 2803 |
. . . 4
β’ {π β£
[(Vtxβπ) /
π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π} = {π β£ βπ β (Vtxβπ)βπ β (Vtxβπ)βπβπ π(π(PathsOnβπ)π)π} |
8 | 7 | eleq2i 2826 |
. . 3
β’ (πΊ β {π β£ [(Vtxβπ) / π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π} β πΊ β {π β£ βπ β (Vtxβπ)βπ β (Vtxβπ)βπβπ π(π(PathsOnβπ)π)π}) |
9 | | fveq2 6892 |
. . . . . 6
β’ (β = πΊ β (Vtxββ) = (VtxβπΊ)) |
10 | | isconngr.v |
. . . . . 6
β’ π = (VtxβπΊ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . 5
β’ (β = πΊ β (Vtxββ) = π) |
12 | | fveq2 6892 |
. . . . . . . . 9
β’ (β = πΊ β (PathsOnββ) = (PathsOnβπΊ)) |
13 | 12 | oveqd 7426 |
. . . . . . . 8
β’ (β = πΊ β (π(PathsOnββ)π) = (π(PathsOnβπΊ)π)) |
14 | 13 | breqd 5160 |
. . . . . . 7
β’ (β = πΊ β (π(π(PathsOnββ)π)π β π(π(PathsOnβπΊ)π)π)) |
15 | 14 | 2exbidv 1928 |
. . . . . 6
β’ (β = πΊ β (βπβπ π(π(PathsOnββ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
16 | 11, 15 | raleqbidv 3343 |
. . . . 5
β’ (β = πΊ β (βπ β (Vtxββ)βπβπ π(π(PathsOnββ)π)π β βπ β π βπβπ π(π(PathsOnβπΊ)π)π)) |
17 | 11, 16 | raleqbidv 3343 |
. . . 4
β’ (β = πΊ β (βπ β (Vtxββ)βπ β (Vtxββ)βπβπ π(π(PathsOnββ)π)π β βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π)) |
18 | | fveq2 6892 |
. . . . . 6
β’ (π = β β (Vtxβπ) = (Vtxββ)) |
19 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π = β β (PathsOnβπ) = (PathsOnββ)) |
20 | 19 | oveqd 7426 |
. . . . . . . . 9
β’ (π = β β (π(PathsOnβπ)π) = (π(PathsOnββ)π)) |
21 | 20 | breqd 5160 |
. . . . . . . 8
β’ (π = β β (π(π(PathsOnβπ)π)π β π(π(PathsOnββ)π)π)) |
22 | 21 | 2exbidv 1928 |
. . . . . . 7
β’ (π = β β (βπβπ π(π(PathsOnβπ)π)π β βπβπ π(π(PathsOnββ)π)π)) |
23 | 18, 22 | raleqbidv 3343 |
. . . . . 6
β’ (π = β β (βπ β (Vtxβπ)βπβπ π(π(PathsOnβπ)π)π β βπ β (Vtxββ)βπβπ π(π(PathsOnββ)π)π)) |
24 | 18, 23 | raleqbidv 3343 |
. . . . 5
β’ (π = β β (βπ β (Vtxβπ)βπ β (Vtxβπ)βπβπ π(π(PathsOnβπ)π)π β βπ β (Vtxββ)βπ β (Vtxββ)βπβπ π(π(PathsOnββ)π)π)) |
25 | 24 | cbvabv 2806 |
. . . 4
β’ {π β£ βπ β (Vtxβπ)βπ β (Vtxβπ)βπβπ π(π(PathsOnβπ)π)π} = {β β£ βπ β (Vtxββ)βπ β (Vtxββ)βπβπ π(π(PathsOnββ)π)π} |
26 | 17, 25 | elab2g 3671 |
. . 3
β’ (πΊ β π β (πΊ β {π β£ βπ β (Vtxβπ)βπ β (Vtxβπ)βπβπ π(π(PathsOnβπ)π)π} β βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π)) |
27 | 8, 26 | bitrid 283 |
. 2
β’ (πΊ β π β (πΊ β {π β£ [(Vtxβπ) / π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π} β βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π)) |
28 | 2, 27 | bitrid 283 |
1
β’ (πΊ β π β (πΊ β ConnGraph β βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π)) |