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

Metamath Proof Explorer

Theorem ushgrunop

Description: The union of two (undirected) simple hypergraphs (with the same vertex set) represented as ordered pair: If <. V , E >. and <. V , F >. are simple hypergraphs, then <. V , E u. F >. is a (not necessarily simple) hypergraph - 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) (Revised by AV, 24-Oct-2021)

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

Proof

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