Theorem usgrun

Description: The union U of two simple graphs G and H with the same vertex set V is a multigraph (not necessarily a simple graph!) with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 29-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		usgrun.g	|- ( ph -> G e. USGraph )
2		usgrun.h	|- ( ph -> H e. USGraph )
3		usgrun.e	|- E = ( iEdg ` G )
4		usgrun.f	|- F = ( iEdg ` H )
5		usgrun.vg	|- V = ( Vtx ` G )
6		usgrun.vh	|- ( ph -> ( Vtx ` H ) = V )
7		usgrun.i	|- ( ph -> ( dom E i^i dom F ) = (/) )
8		usgrun.u	|- ( ph -> U e. W )
9		usgrun.v	|- ( ph -> ( Vtx ` U ) = V )
10		usgrun.un	|- ( ph -> ( iEdg ` U ) = ( E u. F ) )
11		usgrumgr	|- ( G e. USGraph -> G e. UMGraph )
12	1 11	syl	|- ( ph -> G e. UMGraph )
13		usgrumgr	|- ( H e. USGraph -> H e. UMGraph )
14	2 13	syl	|- ( ph -> H e. UMGraph )
15	12 14 3 4 5 6 7 8 9 10	umgrun	|- ( ph -> U e. UMGraph )