Theorem umgrun

Description: The union U of two multigraphs G and H with the same vertex set V is a multigraph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed 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$$
	umgrun.u	$$⊢\phi \to U\in W$$
	umgrun.v	$$⊢\phi \to \mathrm{Vtx}\left(U\right)=V$$
	umgrun.un	$$⊢\phi \to \mathrm{iEdg}\left(U\right)=E\cup F$$
Assertion	umgrun	$$⊢\phi \to U\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		umgrun.u	$$⊢\phi \to U\in W$$
9		umgrun.v	$$⊢\phi \to \mathrm{Vtx}\left(U\right)=V$$
10		umgrun.un	$$⊢\phi \to \mathrm{iEdg}\left(U\right)=E\cup F$$
11	5 3	umgrf	$$⊢G\in \mathrm{UMGraph}\to E:\mathrm{dom}E⟶\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
12	1 11	syl	$$⊢\phi \to E:\mathrm{dom}E⟶\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
13		eqid	$$⊢\mathrm{Vtx}\left(H\right)=\mathrm{Vtx}\left(H\right)$$
14	13 4	umgrf	$$⊢H\in \mathrm{UMGraph}\to F:\mathrm{dom}F⟶\left\{x\in 𝒫\mathrm{Vtx}\left(H\right)|\left|x\right|=2\right\}$$
15	2 14	syl	$$⊢\phi \to F:\mathrm{dom}F⟶\left\{x\in 𝒫\mathrm{Vtx}\left(H\right)|\left|x\right|=2\right\}$$
16	6	eqcomd	$$⊢\phi \to V=\mathrm{Vtx}\left(H\right)$$
17	16	pweqd	$$⊢\phi \to 𝒫V=𝒫\mathrm{Vtx}\left(H\right)$$
18	17	rabeqdv	$$⊢\phi \to \left\{x\in 𝒫V|\left|x\right|=2\right\}=\left\{x\in 𝒫\mathrm{Vtx}\left(H\right)|\left|x\right|=2\right\}$$
19	18	feq3d	$$⊢\phi \to \left(F:\mathrm{dom}F⟶\left\{x\in 𝒫V|\left|x\right|=2\right\}\leftrightarrow F:\mathrm{dom}F⟶\left\{x\in 𝒫\mathrm{Vtx}\left(H\right)|\left|x\right|=2\right\}\right)$$
20	15 19	mpbird	$$⊢\phi \to F:\mathrm{dom}F⟶\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
21	12 20 7	fun2d	$$⊢\phi \to \left(E\cup F\right):\mathrm{dom}E\cup \mathrm{dom}F⟶\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
22	10	dmeqd	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(U\right)=\mathrm{dom}\left(E\cup F\right)$$
23		dmun	$$⊢\mathrm{dom}\left(E\cup F\right)=\mathrm{dom}E\cup \mathrm{dom}F$$
24	22 23	syl6eq	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(U\right)=\mathrm{dom}E\cup \mathrm{dom}F$$
25	9	pweqd	$$⊢\phi \to 𝒫\mathrm{Vtx}\left(U\right)=𝒫V$$
26	25	rabeqdv	$$⊢\phi \to \left\{x\in 𝒫\mathrm{Vtx}\left(U\right)|\left|x\right|=2\right\}=\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
27	10 24 26	feq123d	$$⊢\phi \to \left(\mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶\left\{x\in 𝒫\mathrm{Vtx}\left(U\right)|\left|x\right|=2\right\}\leftrightarrow \left(E\cup F\right):\mathrm{dom}E\cup \mathrm{dom}F⟶\left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$
28	21 27	mpbird	$$⊢\phi \to \mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶\left\{x\in 𝒫\mathrm{Vtx}\left(U\right)|\left|x\right|=2\right\}$$
29		eqid	$$⊢\mathrm{Vtx}\left(U\right)=\mathrm{Vtx}\left(U\right)$$
30		eqid	$$⊢\mathrm{iEdg}\left(U\right)=\mathrm{iEdg}\left(U\right)$$
31	29 30	isumgrs	$$⊢U\in W\to \left(U\in \mathrm{UMGraph}\leftrightarrow \mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶\left\{x\in 𝒫\mathrm{Vtx}\left(U\right)|\left|x\right|=2\right\}\right)$$
32	8 31	syl	$$⊢\phi \to \left(U\in \mathrm{UMGraph}\leftrightarrow \mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶\left\{x\in 𝒫\mathrm{Vtx}\left(U\right)|\left|x\right|=2\right\}\right)$$
33	28 32	mpbird	$$⊢\phi \to U\in \mathrm{UMGraph}$$