| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2731 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
| 2 | | eqid 2731 |
. . . 4
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
| 3 | 1, 2 | uhgrf 28590 |
. . 3
β’ (πΊ β UHGraph β
(iEdgβπΊ):dom
(iEdgβπΊ)βΆ(π« (VtxβπΊ) β
{β
})) |
| 4 | | pweq 4616 |
. . . . . . . 8
β’
((VtxβπΊ) =
β
β π« (VtxβπΊ) = π« β
) |
| 5 | 4 | difeq1d 4121 |
. . . . . . 7
β’
((VtxβπΊ) =
β
β (π« (VtxβπΊ) β {β
}) = (π« β
β {β
})) |
| 6 | | pw0 4815 |
. . . . . . . . 9
β’ π«
β
= {β
} |
| 7 | 6 | difeq1i 4118 |
. . . . . . . 8
β’
(π« β
β {β
}) = ({β
} β
{β
}) |
| 8 | | difid 4370 |
. . . . . . . 8
β’
({β
} β {β
}) = β
|
| 9 | 7, 8 | eqtri 2759 |
. . . . . . 7
β’
(π« β
β {β
}) = β
|
| 10 | 5, 9 | eqtrdi 2787 |
. . . . . 6
β’
((VtxβπΊ) =
β
β (π« (VtxβπΊ) β {β
}) =
β
) |
| 11 | 10 | adantl 481 |
. . . . 5
β’ ((πΊ β π β§ (VtxβπΊ) = β
) β (π«
(VtxβπΊ) β
{β
}) = β
) |
| 12 | 11 | feq3d 6704 |
. . . 4
β’ ((πΊ β π β§ (VtxβπΊ) = β
) β ((iEdgβπΊ):dom (iEdgβπΊ)βΆ(π«
(VtxβπΊ) β
{β
}) β (iEdgβπΊ):dom (iEdgβπΊ)βΆβ
)) |
| 13 | | f00 6773 |
. . . . 5
β’
((iEdgβπΊ):dom
(iEdgβπΊ)βΆβ
β ((iEdgβπΊ) = β
β§ dom
(iEdgβπΊ) =
β
)) |
| 14 | 13 | simplbi 497 |
. . . 4
β’
((iEdgβπΊ):dom
(iEdgβπΊ)βΆβ
β (iEdgβπΊ) = β
) |
| 15 | 12, 14 | syl6bi 253 |
. . 3
β’ ((πΊ β π β§ (VtxβπΊ) = β
) β ((iEdgβπΊ):dom (iEdgβπΊ)βΆ(π«
(VtxβπΊ) β
{β
}) β (iEdgβπΊ) = β
)) |
| 16 | 3, 15 | syl5 34 |
. 2
β’ ((πΊ β π β§ (VtxβπΊ) = β
) β (πΊ β UHGraph β (iEdgβπΊ) = β
)) |
| 17 | | simpl 482 |
. . . . 5
β’ ((πΊ β π β§ (iEdgβπΊ) = β
) β πΊ β π) |
| 18 | | simpr 484 |
. . . . 5
β’ ((πΊ β π β§ (iEdgβπΊ) = β
) β (iEdgβπΊ) = β
) |
| 19 | 17, 18 | uhgr0e 28599 |
. . . 4
β’ ((πΊ β π β§ (iEdgβπΊ) = β
) β πΊ β UHGraph) |
| 20 | 19 | ex 412 |
. . 3
β’ (πΊ β π β ((iEdgβπΊ) = β
β πΊ β UHGraph)) |
| 21 | 20 | adantr 480 |
. 2
β’ ((πΊ β π β§ (VtxβπΊ) = β
) β ((iEdgβπΊ) = β
β πΊ β
UHGraph)) |
| 22 | 16, 21 | impbid 211 |
1
β’ ((πΊ β π β§ (VtxβπΊ) = β
) β (πΊ β UHGraph β (iEdgβπΊ) = β
)) |
