This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrun

Description: The union U of two simple graphs G and H with the same vertex set V is a multigraph (not necessarily a simple graph!) with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 29-Nov-2020)

Ref Expression
Hypotheses usgrun.g ⊢ φ → G ∈ USGraph
usgrun.h ⊢ φ → H ∈ USGraph
usgrun.e ⊢ E = iEdg ⁡ G
usgrun.f ⊢ F = iEdg ⁡ H
usgrun.vg ⊢ V = Vtx ⁡ G
usgrun.vh ⊢ φ → Vtx ⁡ H = V
usgrun.i ⊢ φ → dom ⁡ E ∩ dom ⁡ F = ∅
usgrun.u ⊢ φ → U ∈ W
usgrun.v ⊢ φ → Vtx ⁡ U = V
usgrun.un ⊢ φ → iEdg ⁡ U = E ∪ F
Assertion usgrun ⊢ φ → U ∈ UMGraph

Proof

Step Hyp Ref Expression
1 usgrun.g ⊢ φ → G ∈ USGraph
2 usgrun.h ⊢ φ → H ∈ USGraph
3 usgrun.e ⊢ E = iEdg ⁡ G
4 usgrun.f ⊢ F = iEdg ⁡ H
5 usgrun.vg ⊢ V = Vtx ⁡ G
6 usgrun.vh ⊢ φ → Vtx ⁡ H = V
7 usgrun.i ⊢ φ → dom ⁡ E ∩ dom ⁡ F = ∅
8 usgrun.u ⊢ φ → U ∈ W
9 usgrun.v ⊢ φ → Vtx ⁡ U = V
10 usgrun.un ⊢ φ → iEdg ⁡ U = E ∪ F
11 usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph
12 1 11 syl ⊢ φ → G ∈ UMGraph
13 usgrumgr ⊢ H ∈ USGraph → H ∈ UMGraph
14 2 13 syl ⊢ φ → H ∈ UMGraph
15 12 14 3 4 5 6 7 8 9 10 umgrun ⊢ φ → U ∈ UMGraph