Metamath Proof Explorer


Theorem usgrunop

Description: The union of two simple graphs (with the same vertex set): If <. V , E >. and <. V , F >. are simple graphs, then <. V , E u. F >. is a multigraph (not necessarily a simple graph!) - the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices. (Contributed by AV, 29-Nov-2020)

Ref Expression
Hypotheses usgrun.g
|- ( ph -> G e. USGraph )
usgrun.h
|- ( ph -> H e. USGraph )
usgrun.e
|- E = ( iEdg ` G )
usgrun.f
|- F = ( iEdg ` H )
usgrun.vg
|- V = ( Vtx ` G )
usgrun.vh
|- ( ph -> ( Vtx ` H ) = V )
usgrun.i
|- ( ph -> ( dom E i^i dom F ) = (/) )
Assertion usgrunop
|- ( ph -> <. V , ( E u. F ) >. e. UMGraph )

Proof

Step Hyp Ref Expression
1 usgrun.g
 |-  ( ph -> G e. USGraph )
2 usgrun.h
 |-  ( ph -> H e. USGraph )
3 usgrun.e
 |-  E = ( iEdg ` G )
4 usgrun.f
 |-  F = ( iEdg ` H )
5 usgrun.vg
 |-  V = ( Vtx ` G )
6 usgrun.vh
 |-  ( ph -> ( Vtx ` H ) = V )
7 usgrun.i
 |-  ( ph -> ( dom E i^i dom F ) = (/) )
8 usgrumgr
 |-  ( G e. USGraph -> G e. UMGraph )
9 1 8 syl
 |-  ( ph -> G e. UMGraph )
10 usgrumgr
 |-  ( H e. USGraph -> H e. UMGraph )
11 2 10 syl
 |-  ( ph -> H e. UMGraph )
12 9 11 3 4 5 6 7 umgrunop
 |-  ( ph -> <. V , ( E u. F ) >. e. UMGraph )