| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2726 |
. . . . 5
β’
(VtxβπΊ) =
(VtxβπΊ) |
| 2 | | eqid 2726 |
. . . . 5
β’
(EdgβπΊ) =
(EdgβπΊ) |
| 3 | 1, 2 | iscplgredg 29182 |
. . . 4
β’ (πΊ β UHGraph β (πΊ β ComplGraph β
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπ β (EdgβπΊ){π, π} β π)) |
| 4 | | simp-4l 780 |
. . . . . . . 8
β’
(((((πΊ β
UHGraph β§ π β
(VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β§ {π, π} β π) β πΊ β UHGraph) |
| 5 | | simpr 484 |
. . . . . . . . . . 11
β’ ((πΊ β UHGraph β§ π β (VtxβπΊ)) β π β (VtxβπΊ)) |
| 6 | | eldifi 4121 |
. . . . . . . . . . 11
β’ (π β ((VtxβπΊ) β {π}) β π β (VtxβπΊ)) |
| 7 | 5, 6 | anim12i 612 |
. . . . . . . . . 10
β’ (((πΊ β UHGraph β§ π β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β (π β (VtxβπΊ) β§ π β (VtxβπΊ))) |
| 8 | 7 | adantr 480 |
. . . . . . . . 9
β’ ((((πΊ β UHGraph β§ π β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β (π β (VtxβπΊ) β§ π β (VtxβπΊ))) |
| 9 | 8 | adantr 480 |
. . . . . . . 8
β’
(((((πΊ β
UHGraph β§ π β
(VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β§ {π, π} β π) β (π β (VtxβπΊ) β§ π β (VtxβπΊ))) |
| 10 | | id 22 |
. . . . . . . . . . 11
β’ (π β (EdgβπΊ) β π β (EdgβπΊ)) |
| 11 | | sseq2 4003 |
. . . . . . . . . . . 12
β’ (π = π β ({π, π} β π β {π, π} β π)) |
| 12 | 11 | adantl 481 |
. . . . . . . . . . 11
β’ ((π β (EdgβπΊ) β§ π = π) β ({π, π} β π β {π, π} β π)) |
| 13 | 10, 12 | rspcedv 3599 |
. . . . . . . . . 10
β’ (π β (EdgβπΊ) β ({π, π} β π β βπ β (EdgβπΊ){π, π} β π)) |
| 14 | 13 | adantl 481 |
. . . . . . . . 9
β’ ((((πΊ β UHGraph β§ π β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β ({π, π} β π β βπ β (EdgβπΊ){π, π} β π)) |
| 15 | 14 | imp 406 |
. . . . . . . 8
β’
(((((πΊ β
UHGraph β§ π β
(VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β§ {π, π} β π) β βπ β (EdgβπΊ){π, π} β π) |
| 16 | 1, 2 | 1pthon2v 29915 |
. . . . . . . 8
β’ ((πΊ β UHGraph β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ βπ β (EdgβπΊ){π, π} β π) β βπβπ π(π(PathsOnβπΊ)π)π) |
| 17 | 4, 9, 15, 16 | syl3anc 1368 |
. . . . . . 7
β’
(((((πΊ β
UHGraph β§ π β
(VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β§ π β (EdgβπΊ)) β§ {π, π} β π) β βπβπ π(π(PathsOnβπΊ)π)π) |
| 18 | 17 | rexlimdva2 3151 |
. . . . . 6
β’ (((πΊ β UHGraph β§ π β (VtxβπΊ)) β§ π β ((VtxβπΊ) β {π})) β (βπ β (EdgβπΊ){π, π} β π β βπβπ π(π(PathsOnβπΊ)π)π)) |
| 19 | 18 | ralimdva 3161 |
. . . . 5
β’ ((πΊ β UHGraph β§ π β (VtxβπΊ)) β (βπ β ((VtxβπΊ) β {π})βπ β (EdgβπΊ){π, π} β π β βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
| 20 | 19 | ralimdva 3161 |
. . . 4
β’ (πΊ β UHGraph β
(βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπ β (EdgβπΊ){π, π} β π β βπ β (VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
| 21 | 3, 20 | sylbid 239 |
. . 3
β’ (πΊ β UHGraph β (πΊ β ComplGraph β
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
| 22 | 21 | imp 406 |
. 2
β’ ((πΊ β UHGraph β§ πΊ β ComplGraph) β
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π) |
| 23 | 1 | isconngr1 29952 |
. . 3
β’ (πΊ β UHGraph β (πΊ β ConnGraph β
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
| 24 | 23 | adantr 480 |
. 2
β’ ((πΊ β UHGraph β§ πΊ β ComplGraph) β
(πΊ β ConnGraph β
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})βπβπ π(π(PathsOnβπΊ)π)π)) |
| 25 | 22, 24 | mpbird 257 |
1
β’ ((πΊ β UHGraph β§ πΊ β ComplGraph) β πΊ β
ConnGraph) |
