Theorem uspgrunop

Description: The union of two simple pseudographs (with the same vertex set): If <. V , E >. and <. V , F >. are simple pseudographs, then <. V , E u. F >. is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices). (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020) (Revised by AV, 24-Oct-2021)

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

Proof

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