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