Theorem usgrunop

Description: The union of two simple graphs (with the same vertex set): If <. V , E >. and <. V , F >. are simple graphs, then <. V , E u. F >. is a multigraph (not necessarily a simple graph!) - 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)

	Ref	Expression
Hypotheses	usgrun.g	$$⊢\phi \to G\in \mathrm{USGraph}$$
	usgrun.h	$$⊢\phi \to H\in \mathrm{USGraph}$$
	usgrun.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
	usgrun.f	$$⊢F=\mathrm{iEdg}\left(H\right)$$
	usgrun.vg	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	usgrun.vh	$$⊢\phi \to \mathrm{Vtx}\left(H\right)=V$$
	usgrun.i	$$⊢\phi \to \mathrm{dom}E\cap \mathrm{dom}F=\varnothing$$
Assertion	usgrunop	$$⊢\phi \to ⟨V,E\cup F⟩\in \mathrm{UMGraph}$$

Proof

Step	Hyp	Ref	Expression
1		usgrun.g	$$⊢\phi \to G\in \mathrm{USGraph}$$
2		usgrun.h	$$⊢\phi \to H\in \mathrm{USGraph}$$
3		usgrun.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
4		usgrun.f	$$⊢F=\mathrm{iEdg}\left(H\right)$$
5		usgrun.vg	$$⊢V=\mathrm{Vtx}\left(G\right)$$
6		usgrun.vh	$$⊢\phi \to \mathrm{Vtx}\left(H\right)=V$$
7		usgrun.i	$$⊢\phi \to \mathrm{dom}E\cap \mathrm{dom}F=\varnothing$$
8		usgrumgr	$$⊢G\in \mathrm{USGraph}\to G\in \mathrm{UMGraph}$$
9	1 8	syl	$$⊢\phi \to G\in \mathrm{UMGraph}$$
10		usgrumgr	$$⊢H\in \mathrm{USGraph}\to H\in \mathrm{UMGraph}$$
11	2 10	syl	$$⊢\phi \to H\in \mathrm{UMGraph}$$
12	9 11 3 4 5 6 7	umgrunop	$$⊢\phi \to ⟨V,E\cup F⟩\in \mathrm{UMGraph}$$