Metamath Proof Explorer

Theorem uhgrun

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

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

Proof

Step Hyp Ref Expression
1 uhgrun.g 
 |-  ( ph -> G e. UHGraph )
2 uhgrun.h 
 |-  ( ph -> H e. UHGraph )
3 uhgrun.e 
 |-  E = ( iEdg ` G )
4 uhgrun.f 
 |-  F = ( iEdg ` H )
5 uhgrun.vg 
 |-  V = ( Vtx ` G )
6 uhgrun.vh 
 |-  ( ph -> ( Vtx ` H ) = V )
7 uhgrun.i 
 |-  ( ph -> ( dom E i^i dom F ) = (/) )
8 uhgrun.u 
 |-  ( ph -> U e. W )
9 uhgrun.v 
 |-  ( ph -> ( Vtx ` U ) = V )
10 uhgrun.un 
 |-  ( ph -> ( iEdg ` U ) = ( E u. F ) )
11 5 3 uhgrf 
 |-  ( G e. UHGraph -> E : dom E --> ( ~P V \ { (/) } ) )
12 1 11 syl 
 |-  ( ph -> E : dom E --> ( ~P V \ { (/) } ) )
13 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
14 13 4 uhgrf 
 |-  ( H e. UHGraph -> F : dom F --> ( ~P ( Vtx ` H ) \ { (/) } ) )
15 2 14 syl 
 |-  ( ph -> F : dom F --> ( ~P ( Vtx ` H ) \ { (/) } ) )
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 feq3d 
 |-  ( ph -> ( F : dom F --> ( ~P V \ { (/) } ) <-> F : dom F --> ( ~P ( Vtx ` H ) \ { (/) } ) ) )
20 15 19 mpbird 
 |-  ( ph -> F : dom F --> ( ~P V \ { (/) } ) )
21 12 20 7 fun2d 
 |-  ( ph -> ( E u. F ) : ( dom E u. dom F ) --> ( ~P V \ { (/) } ) )
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 difeq1d 
 |-  ( ph -> ( ~P ( Vtx ` U ) \ { (/) } ) = ( ~P V \ { (/) } ) )
27 10 24 26 feq123d 
 |-  ( ph -> ( ( iEdg ` U ) : dom ( iEdg ` U ) --> ( ~P ( Vtx ` U ) \ { (/) } ) <-> ( E u. F ) : ( dom E u. dom F ) --> ( ~P V \ { (/) } ) ) )
28 21 27 mpbird 
 |-  ( ph -> ( iEdg ` U ) : dom ( iEdg ` U ) --> ( ~P ( Vtx ` U ) \ { (/) } ) )
29 eqid 
 |-  ( Vtx ` U ) = ( Vtx ` U )
30 eqid 
 |-  ( iEdg ` U ) = ( iEdg ` U )
31 29 30 isuhgr 
 |-  ( U e. W -> ( U e. UHGraph <-> ( iEdg ` U ) : dom ( iEdg ` U ) --> ( ~P ( Vtx ` U ) \ { (/) } ) ) )
32 8 31 syl 
 |-  ( ph -> ( U e. UHGraph <-> ( iEdg ` U ) : dom ( iEdg ` U ) --> ( ~P ( Vtx ` U ) \ { (/) } ) ) )
33 28 32 mpbird 
 |-  ( ph -> U e. UHGraph )