Metamath Proof Explorer

Theorem umgrunop

Description: The union of two multigraphs (with the same vertex set): If <. V , E >. and <. V , F >. are multigraphs, then <. V , E u. F >. is a multigraph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 25-Nov-2020)

Ref Expression
Hypotheses umgrun.g ⊢ φ → G ∈ UMGraph
umgrun.h ⊢ φ → H ∈ UMGraph
umgrun.e ⊢ E = iEdg ⁡ G
umgrun.f ⊢ F = iEdg ⁡ H
umgrun.vg ⊢ V = Vtx ⁡ G
umgrun.vh ⊢ φ → Vtx ⁡ H = V
umgrun.i ⊢ φ → dom ⁡ E ∩ dom ⁡ F = ∅
Assertion umgrunop ⊢ φ → V E ∪ F ∈ UMGraph

Proof

Step Hyp Ref Expression
1 umgrun.g ⊢ φ → G ∈ UMGraph
2 umgrun.h ⊢ φ → H ∈ UMGraph
3 umgrun.e ⊢ E = iEdg ⁡ G
4 umgrun.f ⊢ F = iEdg ⁡ H
5 umgrun.vg ⊢ V = Vtx ⁡ G
6 umgrun.vh ⊢ φ → Vtx ⁡ H = V
7 umgrun.i ⊢ φ → dom ⁡ E ∩ dom ⁡ F = ∅
8 opex ⊢ V E ∪ F ∈ V
9 8 a1i ⊢ φ → V E ∪ F ∈ V
10 5 fvexi ⊢ V ∈ V
11 3 fvexi ⊢ E ∈ V
12 4 fvexi ⊢ F ∈ V
13 11 12 unex ⊢ E ∪ F ∈ V
14 10 13 pm3.2i ⊢ V ∈ V ∧ E ∪ F ∈ V
15 opvtxfv ⊢ V ∈ V ∧ E ∪ F ∈ V → Vtx ⁡ V E ∪ F = V
16 14 15 mp1i ⊢ φ → Vtx ⁡ V E ∪ F = V
17 opiedgfv ⊢ V ∈ V ∧ E ∪ F ∈ V → iEdg ⁡ V E ∪ F = E ∪ F
18 14 17 mp1i ⊢ φ → iEdg ⁡ V E ∪ F = E ∪ F
19 1 2 3 4 5 6 7 9 16 18 umgrun ⊢ φ → V E ∪ F ∈ UMGraph