Metamath Proof Explorer

Theorem umgrun

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 
|- ( ph -> G e. UMGraph )
umgrun.h 
|- ( ph -> H e. UMGraph )
umgrun.e 
|- E = ( iEdg ` G )
umgrun.f 
|- F = ( iEdg ` H )
umgrun.vg 
|- V = ( Vtx ` G )
umgrun.vh 
|- ( ph -> ( Vtx ` H ) = V )
umgrun.i 
|- ( ph -> ( dom E i^i dom F ) = (/) )
umgrun.u 
|- ( ph -> U e. W )
umgrun.v 
|- ( ph -> ( Vtx ` U ) = V )
umgrun.un 
|- ( ph -> ( iEdg ` U ) = ( E u. F ) )
Assertion umgrun 
|- ( ph -> U e. UMGraph )

Proof

Step Hyp Ref Expression
1 umgrun.g 
 |-  ( ph -> G e. UMGraph )
2 umgrun.h 
 |-  ( ph -> H e. UMGraph )
3 umgrun.e 
 |-  E = ( iEdg ` G )
4 umgrun.f 
 |-  F = ( iEdg ` H )
5 umgrun.vg 
 |-  V = ( Vtx ` G )
6 umgrun.vh 
 |-  ( ph -> ( Vtx ` H ) = V )
7 umgrun.i 
 |-  ( ph -> ( dom E i^i dom F ) = (/) )
8 umgrun.u 
 |-  ( ph -> U e. W )
9 umgrun.v 
 |-  ( ph -> ( Vtx ` U ) = V )
10 umgrun.un 
 |-  ( ph -> ( iEdg ` U ) = ( E u. F ) )
11 5 3 umgrf 
 |-  ( G e. UMGraph -> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } )
12 1 11 syl 
 |-  ( ph -> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } )
13 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
14 13 4 umgrf 
 |-  ( H e. UMGraph -> F : dom F --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
15 2 14 syl 
 |-  ( ph -> F : dom F --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
16 6 eqcomd 
 |-  ( ph -> V = ( Vtx ` H ) )
17 16 pweqd 
 |-  ( ph -> ~P V = ~P ( Vtx ` H ) )
18 17 rabeqdv 
 |-  ( ph -> { x e. ~P V | ( # ` x ) = 2 } = { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
19 18 feq3d 
 |-  ( ph -> ( F : dom F --> { x e. ~P V | ( # ` x ) = 2 } <-> F : dom F --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) )
20 15 19 mpbird 
 |-  ( ph -> F : dom F --> { x e. ~P V | ( # ` x ) = 2 } )
21 12 20 7 fun2d 
 |-  ( ph -> ( E u. F ) : ( dom E u. dom F ) --> { x e. ~P V | ( # ` x ) = 2 } )
22 10 dmeqd 
 |-  ( ph -> dom ( iEdg ` U ) = dom ( E u. F ) )
23 dmun 
 |-  dom ( E u. F ) = ( dom E u. dom F )
24 22 23 eqtrdi 
 |-  ( ph -> dom ( iEdg ` U ) = ( dom E u. dom F ) )
25 9 pweqd 
 |-  ( ph -> ~P ( Vtx ` U ) = ~P V )
26 25 rabeqdv 
 |-  ( ph -> { x e. ~P ( Vtx ` U ) | ( # ` x ) = 2 } = { x e. ~P V | ( # ` x ) = 2 } )
27 10 24 26 feq123d 
 |-  ( ph -> ( ( iEdg ` U ) : dom ( iEdg ` U ) --> { x e. ~P ( Vtx ` U ) | ( # ` x ) = 2 } <-> ( E u. F ) : ( dom E u. dom F ) --> { x e. ~P V | ( # ` x ) = 2 } ) )
28 21 27 mpbird 
 |-  ( ph -> ( iEdg ` U ) : dom ( iEdg ` U ) --> { x e. ~P ( Vtx ` U ) | ( # ` x ) = 2 } )
29 eqid 
 |-  ( Vtx ` U ) = ( Vtx ` U )
30 eqid 
 |-  ( iEdg ` U ) = ( iEdg ` U )
31 29 30 isumgrs 
 |-  ( U e. W -> ( U e. UMGraph <-> ( iEdg ` U ) : dom ( iEdg ` U ) --> { x e. ~P ( Vtx ` U ) | ( # ` x ) = 2 } ) )
32 8 31 syl 
 |-  ( ph -> ( U e. UMGraph <-> ( iEdg ` U ) : dom ( iEdg ` U ) --> { x e. ~P ( Vtx ` U ) | ( # ` x ) = 2 } ) )
33 28 32 mpbird 
 |-  ( ph -> U e. UMGraph )