Step | Hyp | Ref
| Expression |
1 | | snidg 4663 |
. . . . . . . . . 10
β’ (π β V β π β {π}) |
2 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β π β {π}) |
3 | | eleq2 2823 |
. . . . . . . . . 10
β’
((VtxβπΊ) =
{π} β (π β (VtxβπΊ) β π β {π})) |
4 | 3 | ad2antll 728 |
. . . . . . . . 9
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β (π β (VtxβπΊ) β π β {π})) |
5 | 2, 4 | mpbird 257 |
. . . . . . . 8
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β π β (VtxβπΊ)) |
6 | | eqid 2733 |
. . . . . . . . 9
β’
(VtxβπΊ) =
(VtxβπΊ) |
7 | 6 | 0pthonv 29413 |
. . . . . . . 8
β’ (π β (VtxβπΊ) β βπβπ π(π(PathsOnβπΊ)π)π) |
8 | 5, 7 | syl 17 |
. . . . . . 7
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β βπβπ π(π(PathsOnβπΊ)π)π) |
9 | | oveq2 7417 |
. . . . . . . . . . 11
β’ (π = π β (π(PathsOnβπΊ)π) = (π(PathsOnβπΊ)π)) |
10 | 9 | breqd 5160 |
. . . . . . . . . 10
β’ (π = π β (π(π(PathsOnβπΊ)π)π β π(π(PathsOnβπΊ)π)π)) |
11 | 10 | 2exbidv 1928 |
. . . . . . . . 9
β’ (π = π β (βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
12 | 11 | ralsng 4678 |
. . . . . . . 8
β’ (π β V β (βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
13 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β (βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
14 | 8, 13 | mpbird 257 |
. . . . . 6
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π) |
15 | | oveq1 7416 |
. . . . . . . . . . 11
β’ (π = π β (π(PathsOnβπΊ)π) = (π(PathsOnβπΊ)π)) |
16 | 15 | breqd 5160 |
. . . . . . . . . 10
β’ (π = π β (π(π(PathsOnβπΊ)π)π β π(π(PathsOnβπΊ)π)π)) |
17 | 16 | 2exbidv 1928 |
. . . . . . . . 9
β’ (π = π β (βπβπ π(π(PathsOnβπΊ)π)π β βπβπ π(π(PathsOnβπΊ)π)π)) |
18 | 17 | ralbidv 3178 |
. . . . . . . 8
β’ (π = π β (βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
19 | 18 | ralsng 4678 |
. . . . . . 7
β’ (π β V β (βπ β {π}βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
20 | 19 | adantr 482 |
. . . . . 6
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β (βπ β {π}βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
21 | 14, 20 | mpbird 257 |
. . . . 5
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β βπ β {π}βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π) |
22 | | raleq 3323 |
. . . . . . 7
β’
((VtxβπΊ) =
{π} β (βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
23 | 22 | raleqbi1dv 3334 |
. . . . . 6
β’
((VtxβπΊ) =
{π} β (βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
24 | 23 | ad2antll 728 |
. . . . 5
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β (βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π β βπ β {π}βπ β {π}βπβπ π(π(PathsOnβπΊ)π)π)) |
25 | 21, 24 | mpbird 257 |
. . . 4
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π) |
26 | 6 | isconngr 29473 |
. . . . 5
β’ (πΊ β π β (πΊ β ConnGraph β βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π)) |
27 | 26 | ad2antrl 727 |
. . . 4
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β (πΊ β ConnGraph β βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπβπ π(π(PathsOnβπΊ)π)π)) |
28 | 25, 27 | mpbird 257 |
. . 3
β’ ((π β V β§ (πΊ β π β§ (VtxβπΊ) = {π})) β πΊ β ConnGraph) |
29 | 28 | ex 414 |
. 2
β’ (π β V β ((πΊ β π β§ (VtxβπΊ) = {π}) β πΊ β ConnGraph)) |
30 | | snprc 4722 |
. . 3
β’ (Β¬
π β V β {π} = β
) |
31 | | eqeq2 2745 |
. . . . 5
β’ ({π} = β
β
((VtxβπΊ) = {π} β (VtxβπΊ) = β
)) |
32 | 31 | anbi2d 630 |
. . . 4
β’ ({π} = β
β ((πΊ β π β§ (VtxβπΊ) = {π}) β (πΊ β π β§ (VtxβπΊ) = β
))) |
33 | | 0vconngr 29477 |
. . . 4
β’ ((πΊ β π β§ (VtxβπΊ) = β
) β πΊ β ConnGraph) |
34 | 32, 33 | syl6bi 253 |
. . 3
β’ ({π} = β
β ((πΊ β π β§ (VtxβπΊ) = {π}) β πΊ β ConnGraph)) |
35 | 30, 34 | sylbi 216 |
. 2
β’ (Β¬
π β V β ((πΊ β π β§ (VtxβπΊ) = {π}) β πΊ β ConnGraph)) |
36 | 29, 35 | pm2.61i 182 |
1
β’ ((πΊ β π β§ (VtxβπΊ) = {π}) β πΊ β ConnGraph) |