Proof of Theorem uhgrun
| Step | Hyp | Ref
| Expression |
| 1 | | uhgrun.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ UHGraph) |
| 2 | | uhgrun.vg |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
| 3 | | uhgrun.e |
. . . . . 6
⊢ 𝐸 = (iEdg‘𝐺) |
| 4 | 2, 3 | uhgrf 29079 |
. . . . 5
⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) |
| 5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) |
| 6 | | uhgrun.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ UHGraph) |
| 7 | | eqid 2737 |
. . . . . . 7
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) |
| 8 | | uhgrun.f |
. . . . . . 7
⊢ 𝐹 = (iEdg‘𝐻) |
| 9 | 7, 8 | uhgrf 29079 |
. . . . . 6
⊢ (𝐻 ∈ UHGraph → 𝐹:dom 𝐹⟶(𝒫 (Vtx‘𝐻) ∖
{∅})) |
| 10 | 6, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:dom 𝐹⟶(𝒫 (Vtx‘𝐻) ∖
{∅})) |
| 11 | | uhgrun.vh |
. . . . . . . . 9
⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) |
| 12 | 11 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 = (Vtx‘𝐻)) |
| 13 | 12 | pweqd 4617 |
. . . . . . 7
⊢ (𝜑 → 𝒫 𝑉 = 𝒫 (Vtx‘𝐻)) |
| 14 | 13 | difeq1d 4125 |
. . . . . 6
⊢ (𝜑 → (𝒫 𝑉 ∖ {∅}) = (𝒫
(Vtx‘𝐻) ∖
{∅})) |
| 15 | 14 | feq3d 6723 |
. . . . 5
⊢ (𝜑 → (𝐹:dom 𝐹⟶(𝒫 𝑉 ∖ {∅}) ↔ 𝐹:dom 𝐹⟶(𝒫 (Vtx‘𝐻) ∖
{∅}))) |
| 16 | 10, 15 | mpbird 257 |
. . . 4
⊢ (𝜑 → 𝐹:dom 𝐹⟶(𝒫 𝑉 ∖ {∅})) |
| 17 | | uhgrun.i |
. . . 4
⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) |
| 18 | 5, 16, 17 | fun2d 6772 |
. . 3
⊢ (𝜑 → (𝐸 ∪ 𝐹):(dom 𝐸 ∪ dom 𝐹)⟶(𝒫 𝑉 ∖ {∅})) |
| 19 | | uhgrun.un |
. . . 4
⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹)) |
| 20 | 19 | dmeqd 5916 |
. . . . 5
⊢ (𝜑 → dom (iEdg‘𝑈) = dom (𝐸 ∪ 𝐹)) |
| 21 | | dmun 5921 |
. . . . 5
⊢ dom
(𝐸 ∪ 𝐹) = (dom 𝐸 ∪ dom 𝐹) |
| 22 | 20, 21 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → dom (iEdg‘𝑈) = (dom 𝐸 ∪ dom 𝐹)) |
| 23 | | uhgrun.v |
. . . . . 6
⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) |
| 24 | 23 | pweqd 4617 |
. . . . 5
⊢ (𝜑 → 𝒫 (Vtx‘𝑈) = 𝒫 𝑉) |
| 25 | 24 | difeq1d 4125 |
. . . 4
⊢ (𝜑 → (𝒫
(Vtx‘𝑈) ∖
{∅}) = (𝒫 𝑉
∖ {∅})) |
| 26 | 19, 22, 25 | feq123d 6725 |
. . 3
⊢ (𝜑 → ((iEdg‘𝑈):dom (iEdg‘𝑈)⟶(𝒫
(Vtx‘𝑈) ∖
{∅}) ↔ (𝐸 ∪
𝐹):(dom 𝐸 ∪ dom 𝐹)⟶(𝒫 𝑉 ∖ {∅}))) |
| 27 | 18, 26 | mpbird 257 |
. 2
⊢ (𝜑 → (iEdg‘𝑈):dom (iEdg‘𝑈)⟶(𝒫
(Vtx‘𝑈) ∖
{∅})) |
| 28 | | uhgrun.u |
. . 3
⊢ (𝜑 → 𝑈 ∈ 𝑊) |
| 29 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝑈) =
(Vtx‘𝑈) |
| 30 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝑈) =
(iEdg‘𝑈) |
| 31 | 29, 30 | isuhgr 29077 |
. . 3
⊢ (𝑈 ∈ 𝑊 → (𝑈 ∈ UHGraph ↔ (iEdg‘𝑈):dom (iEdg‘𝑈)⟶(𝒫
(Vtx‘𝑈) ∖
{∅}))) |
| 32 | 28, 31 | syl 17 |
. 2
⊢ (𝜑 → (𝑈 ∈ UHGraph ↔ (iEdg‘𝑈):dom (iEdg‘𝑈)⟶(𝒫
(Vtx‘𝑈) ∖
{∅}))) |
| 33 | 27, 32 | mpbird 257 |
1
⊢ (𝜑 → 𝑈 ∈ UHGraph) |