Theorem upgrun

Description: The union U of two 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, 12-Oct-2020) (Revised by AV, 24-Oct-2021)

	Ref	Expression
Hypotheses	upgrun.g	$$⊢\phi \to G\in \mathrm{UPGraph}$$
	upgrun.h	$$⊢\phi \to H\in \mathrm{UPGraph}$$
	upgrun.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
	upgrun.f	$$⊢F=\mathrm{iEdg}\left(H\right)$$
	upgrun.vg	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	upgrun.vh	$$⊢\phi \to \mathrm{Vtx}\left(H\right)=V$$
	upgrun.i	$$⊢\phi \to \mathrm{dom}E\cap \mathrm{dom}F=\varnothing$$
	upgrun.u	$$⊢\phi \to U\in W$$
	upgrun.v	$$⊢\phi \to \mathrm{Vtx}\left(U\right)=V$$
	upgrun.un	$$⊢\phi \to \mathrm{iEdg}\left(U\right)=E\cup F$$
Assertion	upgrun	$$⊢\phi \to U\in \mathrm{UPGraph}$$

Proof

Step	Hyp	Ref	Expression
1		upgrun.g	$$⊢\phi \to G\in \mathrm{UPGraph}$$
2		upgrun.h	$$⊢\phi \to H\in \mathrm{UPGraph}$$
3		upgrun.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
4		upgrun.f	$$⊢F=\mathrm{iEdg}\left(H\right)$$
5		upgrun.vg	$$⊢V=\mathrm{Vtx}\left(G\right)$$
6		upgrun.vh	$$⊢\phi \to \mathrm{Vtx}\left(H\right)=V$$
7		upgrun.i	$$⊢\phi \to \mathrm{dom}E\cap \mathrm{dom}F=\varnothing$$
8		upgrun.u	$$⊢\phi \to U\in W$$
9		upgrun.v	$$⊢\phi \to \mathrm{Vtx}\left(U\right)=V$$
10		upgrun.un	$$⊢\phi \to \mathrm{iEdg}\left(U\right)=E\cup F$$
11	5 3	upgrf	$$⊢G\in \mathrm{UPGraph}\to E:\mathrm{dom}E⟶\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
12	1 11	syl	$$⊢\phi \to E:\mathrm{dom}E⟶\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
13		eqid	$$⊢\mathrm{Vtx}\left(H\right)=\mathrm{Vtx}\left(H\right)$$
14	13 4	upgrf	$$⊢H\in \mathrm{UPGraph}\to F:\mathrm{dom}F⟶\left\{x\in \left(𝒫\mathrm{Vtx}\left(H\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
15	2 14	syl	$$⊢\phi \to F:\mathrm{dom}F⟶\left\{x\in \left(𝒫\mathrm{Vtx}\left(H\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 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	difeq1d	$$⊢\phi \to 𝒫V\setminus \left\{\varnothing \right\}=𝒫\mathrm{Vtx}\left(H\right)\setminus \left\{\varnothing \right\}$$
19	18	rabeqdv	$$⊢\phi \to \left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}=\left\{x\in \left(𝒫\mathrm{Vtx}\left(H\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
20	19	feq3d	$$⊢\phi \to \left(F:\mathrm{dom}F⟶\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\leftrightarrow F:\mathrm{dom}F⟶\left\{x\in \left(𝒫\mathrm{Vtx}\left(H\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\right)$$
21	15 20	mpbird	$$⊢\phi \to F:\mathrm{dom}F⟶\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
22	12 21 7	fun2d	$$⊢\phi \to \left(E\cup F\right):\mathrm{dom}E\cup \mathrm{dom}F⟶\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
23	10	dmeqd	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(U\right)=\mathrm{dom}\left(E\cup F\right)$$
24		dmun	$$⊢\mathrm{dom}\left(E\cup F\right)=\mathrm{dom}E\cup \mathrm{dom}F$$
25	23 24	eqtrdi	$$⊢\phi \to \mathrm{dom}\mathrm{iEdg}\left(U\right)=\mathrm{dom}E\cup \mathrm{dom}F$$
26	9	pweqd	$$⊢\phi \to 𝒫\mathrm{Vtx}\left(U\right)=𝒫V$$
27	26	difeq1d	$$⊢\phi \to 𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \right\}=𝒫V\setminus \left\{\varnothing \right\}$$
28	27	rabeqdv	$$⊢\phi \to \left\{x\in \left(𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}=\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
29	10 25 28	feq123d	$$⊢\phi \to \left(\mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶\left\{x\in \left(𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\leftrightarrow \left(E\cup F\right):\mathrm{dom}E\cup \mathrm{dom}F⟶\left\{x\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\right)$$
30	22 29	mpbird	$$⊢\phi \to \mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶\left\{x\in \left(𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}$$
31		eqid	$$⊢\mathrm{Vtx}\left(U\right)=\mathrm{Vtx}\left(U\right)$$
32		eqid	$$⊢\mathrm{iEdg}\left(U\right)=\mathrm{iEdg}\left(U\right)$$
33	31 32	isupgr	$$⊢U\in W\to \left(U\in \mathrm{UPGraph}\leftrightarrow \mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶\left\{x\in \left(𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\right)$$
34	8 33	syl	$$⊢\phi \to \left(U\in \mathrm{UPGraph}\leftrightarrow \mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶\left\{x\in \left(𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \right\}\right)|\left|x\right|\le 2\right\}\right)$$
35	30 34	mpbird	$$⊢\phi \to U\in \mathrm{UPGraph}$$