Theorem uspgrun

Description: The union U of two simple pseudographs G and H with the same vertex set V is a pseudograph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 16-Oct-2020)

	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$$
	uspgrun.u	$$⊢\phi \to U\in W$$
	uspgrun.v	$$⊢\phi \to \mathrm{Vtx}\left(U\right)=V$$
	uspgrun.un	$$⊢\phi \to \mathrm{iEdg}\left(U\right)=E\cup F$$
Assertion	uspgrun	$$⊢\phi \to U\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		uspgrun.u	$$⊢\phi \to U\in W$$
9		uspgrun.v	$$⊢\phi \to \mathrm{Vtx}\left(U\right)=V$$
10		uspgrun.un	$$⊢\phi \to \mathrm{iEdg}\left(U\right)=E\cup F$$
11		uspgrupgr	$$⊢G\in \mathrm{USHGraph}\to G\in \mathrm{UPGraph}$$
12	1 11	syl	$$⊢\phi \to G\in \mathrm{UPGraph}$$
13		uspgrupgr	$$⊢H\in \mathrm{USHGraph}\to H\in \mathrm{UPGraph}$$
14	2 13	syl	$$⊢\phi \to H\in \mathrm{UPGraph}$$
15	12 14 3 4 5 6 7 8 9 10	upgrun	$$⊢\phi \to U\in \mathrm{UPGraph}$$