Metamath Proof Explorer


Theorem upgrunop

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

Ref Expression
Hypotheses upgrun.g φGUPGraph
upgrun.h φHUPGraph
upgrun.e E=iEdgG
upgrun.f F=iEdgH
upgrun.vg V=VtxG
upgrun.vh φVtxH=V
upgrun.i φdomEdomF=
Assertion upgrunop φVEFUPGraph

Proof

Step Hyp Ref Expression
1 upgrun.g φGUPGraph
2 upgrun.h φHUPGraph
3 upgrun.e E=iEdgG
4 upgrun.f F=iEdgH
5 upgrun.vg V=VtxG
6 upgrun.vh φVtxH=V
7 upgrun.i φdomEdomF=
8 opex VEFV
9 8 a1i φVEFV
10 5 fvexi VV
11 3 fvexi EV
12 4 fvexi FV
13 11 12 unex EFV
14 10 13 pm3.2i VVEFV
15 opvtxfv VVEFVVtxVEF=V
16 14 15 mp1i φVtxVEF=V
17 opiedgfv VVEFViEdgVEF=EF
18 14 17 mp1i φiEdgVEF=EF
19 1 2 3 4 5 6 7 9 16 18 upgrun φVEFUPGraph