This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uspgrunop

Description: The union of two simple pseudographs (with the same vertex set): If <. V , E >. and <. V , F >. are simple pseudographs, then <. V , E u. F >. is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting in two edges between two vertices). (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020) (Revised by AV, 24-Oct-2021)

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

Proof

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