Metamath Proof Explorer

Theorem upgrun

Description: The union U of two pseudographs G and H with the same vertex set V is a pseudograph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 12-Oct-2020) (Revised by AV, 24-Oct-2021)

Ref Expression
Hypotheses upgrun.g 
|- ( ph -> G e. UPGraph )
upgrun.h 
|- ( ph -> H e. UPGraph )
upgrun.e 
|- E = ( iEdg ` G )
upgrun.f 
|- F = ( iEdg ` H )
upgrun.vg 
|- V = ( Vtx ` G )
upgrun.vh 
|- ( ph -> ( Vtx ` H ) = V )
upgrun.i 
|- ( ph -> ( dom E i^i dom F ) = (/) )
upgrun.u 
|- ( ph -> U e. W )
upgrun.v 
|- ( ph -> ( Vtx ` U ) = V )
upgrun.un 
|- ( ph -> ( iEdg ` U ) = ( E u. F ) )
Assertion upgrun 
|- ( ph -> U e. UPGraph )

Proof

Step Hyp Ref Expression
1 upgrun.g 
 |-  ( ph -> G e. UPGraph )
2 upgrun.h 
 |-  ( ph -> H e. UPGraph )
3 upgrun.e 
 |-  E = ( iEdg ` G )
4 upgrun.f 
 |-  F = ( iEdg ` H )
5 upgrun.vg 
 |-  V = ( Vtx ` G )
6 upgrun.vh 
 |-  ( ph -> ( Vtx ` H ) = V )
7 upgrun.i 
 |-  ( ph -> ( dom E i^i dom F ) = (/) )
8 upgrun.u 
 |-  ( ph -> U e. W )
9 upgrun.v 
 |-  ( ph -> ( Vtx ` U ) = V )
10 upgrun.un 
 |-  ( ph -> ( iEdg ` U ) = ( E u. F ) )
11 5 3 upgrf 
 |-  ( G e. UPGraph -> 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 upgrf 
 |-  ( H e. UPGraph -> 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 difeq1d 
 |-  ( ph -> ( ~P V \ { (/) } ) = ( ~P ( Vtx ` H ) \ { (/) } ) )
19 18 rabeqdv 
 |-  ( ph -> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } = { x e. ( ~P ( Vtx ` H ) \ { (/) } ) | ( # ` x ) <_ 2 } )
20 19 feq3d 
 |-  ( ph -> ( F : dom F --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } <-> F : dom F --> { x e. ( ~P ( Vtx ` H ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
21 15 20 mpbird 
 |-  ( ph -> F : dom F --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
22 12 21 7 fun2d 
 |-  ( ph -> ( E u. F ) : ( dom E u. dom F ) --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
23 10 dmeqd 
 |-  ( ph -> dom ( iEdg ` U ) = dom ( E u. F ) )
24 dmun 
 |-  dom ( E u. F ) = ( dom E u. dom F )
25 23 24 eqtrdi 
 |-  ( ph -> dom ( iEdg ` U ) = ( dom E u. dom F ) )
26 9 pweqd 
 |-  ( ph -> ~P ( Vtx ` U ) = ~P V )
27 26 difeq1d 
 |-  ( ph -> ( ~P ( Vtx ` U ) \ { (/) } ) = ( ~P V \ { (/) } ) )
28 27 rabeqdv 
 |-  ( ph -> { x e. ( ~P ( Vtx ` U ) \ { (/) } ) | ( # ` x ) <_ 2 } = { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
29 10 25 28 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 } ) )
30 22 29 mpbird 
 |-  ( ph -> ( iEdg ` U ) : dom ( iEdg ` U ) --> { x e. ( ~P ( Vtx ` U ) \ { (/) } ) | ( # ` x ) <_ 2 } )
31 eqid 
 |-  ( Vtx ` U ) = ( Vtx ` U )
32 eqid 
 |-  ( iEdg ` U ) = ( iEdg ` U )
33 31 32 isupgr 
 |-  ( U e. W -> ( U e. UPGraph <-> ( iEdg ` U ) : dom ( iEdg ` U ) --> { x e. ( ~P ( Vtx ` U ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
34 8 33 syl 
 |-  ( ph -> ( U e. UPGraph <-> ( iEdg ` U ) : dom ( iEdg ` U ) --> { x e. ( ~P ( Vtx ` U ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
35 30 34 mpbird 
 |-  ( ph -> U e. UPGraph )