Theorem umgrunop

Description: The union of two multigraphs (with the same vertex set): If <. V , E >. and <. V , F >. are multigraphs, then <. V , E u. F >. is a multigraph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 25-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		umgrun.g	$$⊢\phi \to G\in \mathrm{UMGraph}$$
2		umgrun.h	$$⊢\phi \to H\in \mathrm{UMGraph}$$
3		umgrun.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
4		umgrun.f	$$⊢F=\mathrm{iEdg}\left(H\right)$$
5		umgrun.vg	$$⊢V=\mathrm{Vtx}\left(G\right)$$
6		umgrun.vh	$$⊢\phi \to \mathrm{Vtx}\left(H\right)=V$$
7		umgrun.i	$$⊢\phi \to \mathrm{dom}E\cap \mathrm{dom}F=\varnothing$$
8		opex	$$⊢⟨V,E\cup F⟩\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to ⟨V,E\cup F⟩\in \mathrm{V}$$
10	5	fvexi	$$⊢V\in \mathrm{V}$$
11	3	fvexi	$$⊢E\in \mathrm{V}$$
12	4	fvexi	$$⊢F\in \mathrm{V}$$
13	11 12	unex	$$⊢E\cup F\in \mathrm{V}$$
14	10 13	pm3.2i	$$⊢\left(V\in \mathrm{V}\wedge E\cup F\in \mathrm{V}\right)$$
15		opvtxfv	$$⊢\left(V\in \mathrm{V}\wedge E\cup F\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨V,E\cup F⟩\right)=V$$
16	14 15	mp1i	$$⊢\phi \to \mathrm{Vtx}\left(⟨V,E\cup F⟩\right)=V$$
17		opiedgfv	$$⊢\left(V\in \mathrm{V}\wedge E\cup F\in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨V,E\cup F⟩\right)=E\cup F$$
18	14 17	mp1i	$$⊢\phi \to \mathrm{iEdg}\left(⟨V,E\cup F⟩\right)=E\cup F$$
19	1 2 3 4 5 6 7 9 16 18	umgrun	$$⊢\phi \to ⟨V,E\cup F⟩\in \mathrm{UMGraph}$$