Step | Hyp | Ref
| Expression |
1 | | snidg 4620 |
. . . . . . . . . 10
β’ (π β V β π β {π}) |
2 | 1 | adantr 481 |
. . . . . . . . 9
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β π β {π}) |
3 | | eleq2 2826 |
. . . . . . . . . 10
β’
((VtxβπΊ) =
{π} β (π β (VtxβπΊ) β π β {π})) |
4 | 3 | ad2antll 727 |
. . . . . . . . 9
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β (π β (VtxβπΊ) β π β {π})) |
5 | 2, 4 | mpbird 256 |
. . . . . . . 8
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β π β (VtxβπΊ)) |
6 | | eqid 2736 |
. . . . . . . . 9
β’
(VtxβπΊ) =
(VtxβπΊ) |
7 | 6 | 0pthonv 29073 |
. . . . . . . 8
β’ (π β (VtxβπΊ) β βπβπ π(π(PathsOnβπΊ)π)π) |
8 | 5, 7 | syl 17 |
. . . . . . 7
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β βπβπ π(π(PathsOnβπΊ)π)π) |
9 | | oveq2 7365 |
. . . . . . . . . . 11
β’ (π = π β (π(PathsOnβπΊ)π) = (π(PathsOnβπΊ)π)) |
10 | 9 | breqd 5116 |
. . . . . . . . . 10
β’ (π = π β (π(π(PathsOnβπΊ)π)π β π(π(PathsOnβπΊ)π)π)) |
11 | 10 | 2exbidv 1927 |
. . . . . . . . 9
β’ (π = π β (βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
12 | 11 | ralsng 4634 |
. . . . . . . 8
β’ (π β V β (βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
13 | 12 | adantr 481 |
. . . . . . 7
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β (βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
14 | 8, 13 | mpbird 256 |
. . . . . 6
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π) |
15 | | oveq1 7364 |
. . . . . . . . . . 11
β’ (π = π β (π(PathsOnβπΊ)π) = (π(PathsOnβπΊ)π)) |
16 | 15 | breqd 5116 |
. . . . . . . . . 10
β’ (π = π β (π(π(PathsOnβπΊ)π)π β π(π(PathsOnβπΊ)π)π)) |
17 | 16 | 2exbidv 1927 |
. . . . . . . . 9
β’ (π = π β (βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
18 | 17 | ralbidv 3174 |
. . . . . . . 8
β’ (π = π β (βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
19 | 18 | ralsng 4634 |
. . . . . . 7
β’ (π β V β (βπ β {π}βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
20 | 19 | adantr 481 |
. . . . . 6
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β (βπ β {π}βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
21 | 14, 20 | mpbird 256 |
. . . . 5
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β βπ β {π}βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π) |
22 | | raleq 3309 |
. . . . . . 7
β’
((VtxβπΊ) =
{π} β (βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
23 | 22 | raleqbi1dv 3307 |
. . . . . 6
β’
((VtxβπΊ) =
{π} β (βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
24 | 23 | ad2antll 727 |
. . . . 5
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β (βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
25 | 21, 24 | mpbird 256 |
. . . 4
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π) |
26 | 6 | isconngr 29133 |
. . . . 5
β’ (πΊ β π β (πΊ β ConnGraph β βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π)) |
27 | 26 | ad2antrl 726 |
. . . 4
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β (πΊ β ConnGraph β βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π)) |
28 | 25, 27 | mpbird 256 |
. . 3
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β πΊ β ConnGraph) |
29 | 28 | ex 413 |
. 2
β’ (π β V β ((πΊ β π β§ (VtxβπΊ) = {π}) β πΊ β ConnGraph)) |
30 | | snprc 4678 |
. . 3
β’ (Β¬
π β V β {π} = β
) |
31 | | eqeq2 2748 |
. . . . 5
β’ ({π} = β
β
((VtxβπΊ) = {π} β (VtxβπΊ) = β
)) |
32 | 31 | anbi2d 629 |
. . . 4
β’ ({π} = β
β ((πΊ β π β§ (VtxβπΊ) = {π}) β (πΊ β π β§ (VtxβπΊ) = β
))) |
33 | | 0vconngr 29137 |
. . . 4
β’ ((πΊ β π β§ (VtxβπΊ) = β
) β πΊ β ConnGraph) |
34 | 32, 33 | syl6bi 252 |
. . 3
β’ ({π} = β
β ((πΊ β π β§ (VtxβπΊ) = {π}) β πΊ β ConnGraph)) |
35 | 30, 34 | sylbi 216 |
. 2
β’ (Β¬
π β V β ((πΊ β π β§ (VtxβπΊ) = {π}) β πΊ β ConnGraph)) |
36 | 29, 35 | pm2.61i 182 |
1
β’ ((πΊ β π β§ (VtxβπΊ) = {π}) β πΊ β ConnGraph) |