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 )