Description: The union U of two multigraphs G and H with the same vertex set V is a multigraph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 25-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | umgrun.g | |
|
umgrun.h | |
||
umgrun.e | |
||
umgrun.f | |
||
umgrun.vg | |
||
umgrun.vh | |
||
umgrun.i | |
||
umgrun.u | |
||
umgrun.v | |
||
umgrun.un | |
||
Assertion | umgrun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | umgrun.g | |
|
2 | umgrun.h | |
|
3 | umgrun.e | |
|
4 | umgrun.f | |
|
5 | umgrun.vg | |
|
6 | umgrun.vh | |
|
7 | umgrun.i | |
|
8 | umgrun.u | |
|
9 | umgrun.v | |
|
10 | umgrun.un | |
|
11 | 5 3 | umgrf | |
12 | 1 11 | syl | |
13 | eqid | |
|
14 | 13 4 | umgrf | |
15 | 2 14 | syl | |
16 | 6 | eqcomd | |
17 | 16 | pweqd | |
18 | 17 | rabeqdv | |
19 | 18 | feq3d | |
20 | 15 19 | mpbird | |
21 | 12 20 7 | fun2d | |
22 | 10 | dmeqd | |
23 | dmun | |
|
24 | 22 23 | eqtrdi | |
25 | 9 | pweqd | |
26 | 25 | rabeqdv | |
27 | 10 24 26 | feq123d | |
28 | 21 27 | mpbird | |
29 | eqid | |
|
30 | eqid | |
|
31 | 29 30 | isumgrs | |
32 | 8 31 | syl | |
33 | 28 32 | mpbird | |