Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | | eqid 2733 |
. . . . 5
β’
(EdgβπΊ) =
(EdgβπΊ) |
3 | 1, 2 | iscplgredg 28674 |
. . . 4
β’ (πΊ β UHGraph β (πΊ β ComplGraph β
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπ β (EdgβπΊ){π, π} β π)) |
4 | | simp-4l 782 |
. . . . . . . 8
β’
(((((πΊ β
UHGraph β§ π β
(VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β§ {π, π} β π) β πΊ β UHGraph) |
5 | | simpr 486 |
. . . . . . . . . . 11
β’ ((πΊ β UHGraph β§ π β (VtxβπΊ)) β π β (VtxβπΊ)) |
6 | | eldifi 4127 |
. . . . . . . . . . 11
β’ (π β ((VtxβπΊ) β {π}) β π β (VtxβπΊ)) |
7 | 5, 6 | anim12i 614 |
. . . . . . . . . 10
β’ (((πΊ β UHGraph β§ π β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β (π β (VtxβπΊ) β§ π β (VtxβπΊ))) |
8 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((((πΊ β UHGraph β§ π β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β (π β (VtxβπΊ) β§ π β (VtxβπΊ))) |
9 | 8 | adantr 482 |
. . . . . . . 8
β’
(((((πΊ β
UHGraph β§ π β
(VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β§ {π, π} β π) β (π β (VtxβπΊ) β§ π β (VtxβπΊ))) |
10 | | id 22 |
. . . . . . . . . . 11
β’ (π β (EdgβπΊ) β π β (EdgβπΊ)) |
11 | | sseq2 4009 |
. . . . . . . . . . . 12
β’ (π = π β ({π, π} β π β {π, π} β π)) |
12 | 11 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β (EdgβπΊ) β§ π = π) β ({π, π} β π β {π, π} β π)) |
13 | 10, 12 | rspcedv 3606 |
. . . . . . . . . 10
β’ (π β (EdgβπΊ) β ({π, π} β π β βπ β (EdgβπΊ){π, π} β π)) |
14 | 13 | adantl 483 |
. . . . . . . . 9
β’ ((((πΊ β UHGraph β§ π β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β ({π, π} β π β βπ β (EdgβπΊ){π, π} β π)) |
15 | 14 | imp 408 |
. . . . . . . 8
β’
(((((πΊ β
UHGraph β§ π β
(VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β§ {π, π} β π) β βπ β (EdgβπΊ){π, π} β π) |
16 | 1, 2 | 1pthon2v 29406 |
. . . . . . . 8
β’ ((πΊ β UHGraph β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ βπ β (EdgβπΊ){π, π} β π) β βπβπ π(π(PathsOnβπΊ)π)π) |
17 | 4, 9, 15, 16 | syl3anc 1372 |
. . . . . . 7
β’
(((((πΊ β
UHGraph β§ π β
(VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β§ {π, π} β π) β βπβπ π(π(PathsOnβπΊ)π)π) |
18 | 17 | rexlimdva2 3158 |
. . . . . 6
β’ (((πΊ β UHGraph β§ π β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β (βπ β (EdgβπΊ){π, π} β π β βπβπ π(π(PathsOnβπΊ)π)π)) |
19 | 18 | ralimdva 3168 |
. . . . 5
β’ ((πΊ β UHGraph β§ π β (VtxβπΊ)) β (βπ β ((VtxβπΊ) β {π})βπ β (EdgβπΊ){π, π} β π β βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
20 | 19 | ralimdva 3168 |
. . . 4
β’ (πΊ β UHGraph β
(βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπ β (EdgβπΊ){π, π} β π β βπ β (VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
21 | 3, 20 | sylbid 239 |
. . 3
β’ (πΊ β UHGraph β (πΊ β ComplGraph β
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
22 | 21 | imp 408 |
. 2
β’ ((πΊ β UHGraph β§ πΊ β ComplGraph) β
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π) |
23 | 1 | isconngr1 29443 |
. . 3
β’ (πΊ β UHGraph β (πΊ β ConnGraph β
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
24 | 23 | adantr 482 |
. 2
β’ ((πΊ β UHGraph β§ πΊ β ComplGraph) β
(πΊ β ConnGraph β
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
25 | 22, 24 | mpbird 257 |
1
β’ ((πΊ β UHGraph β§ πΊ β ComplGraph) β πΊ β
ConnGraph) |