Step | Hyp | Ref
| Expression |
1 | | dfconngr1 28840 |
. . 3
β’ ConnGraph
= {π β£
[(Vtxβπ) /
π£]βπ β π£ βπ β (π£ β {π})βπβπ π(π(PathsOnβπ)π)π} |
2 | 1 | eleq2i 2828 |
. 2
β’ (πΊ β ConnGraph β πΊ β {π β£ [(Vtxβπ) / π£]βπ β π£ βπ β (π£ β {π})βπβπ π(π(PathsOnβπ)π)π}) |
3 | | fvex 6838 |
. . . . . 6
β’
(Vtxβπ) β
V |
4 | | id 22 |
. . . . . . 7
β’ (π£ = (Vtxβπ) β π£ = (Vtxβπ)) |
5 | | difeq1 4062 |
. . . . . . . 8
β’ (π£ = (Vtxβπ) β (π£ β {π}) = ((Vtxβπ) β {π})) |
6 | 5 | raleqdv 3309 |
. . . . . . 7
β’ (π£ = (Vtxβπ) β (βπ β (π£ β {π})βπβπ π(π(PathsOnβπ)π)π β βπ β ((Vtxβπ) β {π})βπβπ π(π(PathsOnβπ)π)π)) |
7 | 4, 6 | raleqbidv 3315 |
. . . . . 6
β’ (π£ = (Vtxβπ) β (βπ β π£ βπ β (π£ β {π})βπβπ π(π(PathsOnβπ)π)π β βπ β (Vtxβπ)βπ β ((Vtxβπ) β {π})βπβπ π(π(PathsOnβπ)π)π)) |
8 | 3, 7 | sbcie 3770 |
. . . . 5
β’
([(Vtxβπ) / π£]βπ β π£ βπ β (π£ β {π})βπβπ π(π(PathsOnβπ)π)π β βπ β (Vtxβπ)βπ β ((Vtxβπ) β {π})βπβπ π(π(PathsOnβπ)π)π) |
9 | 8 | abbii 2806 |
. . . 4
β’ {π β£
[(Vtxβπ) /
π£]βπ β π£ βπ β (π£ β {π})βπβπ π(π(PathsOnβπ)π)π} = {π β£ βπ β (Vtxβπ)βπ β ((Vtxβπ) β {π})βπβπ π(π(PathsOnβπ)π)π} |
10 | 9 | eleq2i 2828 |
. . 3
β’ (πΊ β {π β£ [(Vtxβπ) / π£]βπ β π£ βπ β (π£ β {π})βπβπ π(π(PathsOnβπ)π)π} β πΊ β {π β£ βπ β (Vtxβπ)βπ β ((Vtxβπ) β {π})βπβπ π(π(PathsOnβπ)π)π}) |
11 | | fveq2 6825 |
. . . . . 6
β’ (β = πΊ β (Vtxββ) = (VtxβπΊ)) |
12 | | isconngr.v |
. . . . . 6
β’ π = (VtxβπΊ) |
13 | 11, 12 | eqtr4di 2794 |
. . . . 5
β’ (β = πΊ β (Vtxββ) = π) |
14 | 13 | difeq1d 4068 |
. . . . . 6
β’ (β = πΊ β ((Vtxββ) β {π}) = (π β {π})) |
15 | | fveq2 6825 |
. . . . . . . . 9
β’ (β = πΊ β (PathsOnββ) = (PathsOnβπΊ)) |
16 | 15 | oveqd 7354 |
. . . . . . . 8
β’ (β = πΊ β (π(PathsOnββ)π) = (π(PathsOnβπΊ)π)) |
17 | 16 | breqd 5103 |
. . . . . . 7
β’ (β = πΊ β (π(π(PathsOnββ)π)π β π(π(PathsOnβπΊ)π)π)) |
18 | 17 | 2exbidv 1926 |
. . . . . 6
β’ (β = πΊ β (βπβπ π(π(PathsOnββ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
19 | 14, 18 | raleqbidv 3315 |
. . . . 5
β’ (β = πΊ β (βπ β ((Vtxββ) β {π})βπβπ π(π(PathsOnββ)π)π β βπ β (π β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
20 | 13, 19 | raleqbidv 3315 |
. . . 4
β’ (β = πΊ β (βπ β (Vtxββ)βπ β ((Vtxββ) β {π})βπβπ π(π(PathsOnββ)π)π β βπ β π βπ β (π β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
21 | | fveq2 6825 |
. . . . . 6
β’ (π = β β (Vtxβπ) = (Vtxββ)) |
22 | 21 | difeq1d 4068 |
. . . . . . 7
β’ (π = β β ((Vtxβπ) β {π}) = ((Vtxββ) β {π})) |
23 | | fveq2 6825 |
. . . . . . . . . 10
β’ (π = β β (PathsOnβπ) = (PathsOnββ)) |
24 | 23 | oveqd 7354 |
. . . . . . . . 9
β’ (π = β β (π(PathsOnβπ)π) = (π(PathsOnββ)π)) |
25 | 24 | breqd 5103 |
. . . . . . . 8
β’ (π = β β (π(π(PathsOnβπ)π)π β π(π(PathsOnββ)π)π)) |
26 | 25 | 2exbidv 1926 |
. . . . . . 7
β’ (π = β β (βπβπ π(π(PathsOnβπ)π)π β βπβπ π(π(PathsOnββ)π)π)) |
27 | 22, 26 | raleqbidv 3315 |
. . . . . 6
β’ (π = β β (βπ β ((Vtxβπ) β {π})βπβπ π(π(PathsOnβπ)π)π β βπ β ((Vtxββ) β {π})βπβπ π(π(PathsOnββ)π)π)) |
28 | 21, 27 | raleqbidv 3315 |
. . . . 5
β’ (π = β β (βπ β (Vtxβπ)βπ β ((Vtxβπ) β {π})βπβπ π(π(PathsOnβπ)π)π β βπ β (Vtxββ)βπ β ((Vtxββ) β {π})βπβπ π(π(PathsOnββ)π)π)) |
29 | 28 | cbvabv 2809 |
. . . 4
β’ {π β£ βπ β (Vtxβπ)βπ β ((Vtxβπ) β {π})βπβπ π(π(PathsOnβπ)π)π} = {β β£ βπ β (Vtxββ)βπ β ((Vtxββ) β {π})βπβπ π(π(PathsOnββ)π)π} |
30 | 20, 29 | elab2g 3621 |
. . 3
β’ (πΊ β π β (πΊ β {π β£ βπ β (Vtxβπ)βπ β ((Vtxβπ) β {π})βπβπ π(π(PathsOnβπ)π)π} β βπ β π βπ β (π β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
31 | 10, 30 | bitrid 282 |
. 2
β’ (πΊ β π β (πΊ β {π β£ [(Vtxβπ) / π£]βπ β π£ βπ β (π£ β {π})βπβπ π(π(PathsOnβπ)π)π} β βπ β π βπ β (π β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
32 | 2, 31 | bitrid 282 |
1
β’ (πΊ β π β (πΊ β ConnGraph β βπ β π βπ β (π β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |