Theorem uhgrun

Description: The union U of two (undirected) hypergraphs G and H with the same vertex set V is a hypergraph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 11-Oct-2020) (Revised by AV, 24-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		uhgrun.g	$$⊢\phi \to G\in \mathrm{UHGraph}$$
2		uhgrun.h	$$⊢\phi \to H\in \mathrm{UHGraph}$$
3		uhgrun.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
4		uhgrun.f	$$⊢F=\mathrm{iEdg}\left(H\right)$$
5		uhgrun.vg	$$⊢V=\mathrm{Vtx}\left(G\right)$$
6		uhgrun.vh	$$⊢\phi \to \mathrm{Vtx}\left(H\right)=V$$
7		uhgrun.i	$$⊢\phi \to \mathrm{dom}E\cap \mathrm{dom}F=\varnothing$$
8		uhgrun.u	$$⊢\phi \to U\in W$$
9		uhgrun.v	$$⊢\phi \to \mathrm{Vtx}\left(U\right)=V$$
10		uhgrun.un	$$⊢\phi \to \mathrm{iEdg}\left(U\right)=E\cup F$$
11	5 3	uhgrf	$$⊢G\in \mathrm{UHGraph}\to E:\mathrm{dom}E⟶𝒫V\setminus \left\{\varnothing \right\}$$
12	1 11	syl	$$⊢\phi \to E:\mathrm{dom}E⟶𝒫V\setminus \left\{\varnothing \right\}$$
13		eqid	$$⊢\mathrm{Vtx}\left(H\right)=\mathrm{Vtx}\left(H\right)$$
14	13 4	uhgrf	$$⊢H\in \mathrm{UHGraph}\to F:\mathrm{dom}F⟶𝒫\mathrm{Vtx}\left(H\right)\setminus \left\{\varnothing \right\}$$
15	2 14	syl	$$⊢\phi \to F:\mathrm{dom}F⟶𝒫\mathrm{Vtx}\left(H\right)\setminus \left\{\varnothing \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	feq3d	$$⊢\phi \to \left(F:\mathrm{dom}F⟶𝒫V\setminus \left\{\varnothing \right\}\leftrightarrow F:\mathrm{dom}F⟶𝒫\mathrm{Vtx}\left(H\right)\setminus \left\{\varnothing \right\}\right)$$
20	15 19	mpbird	$$⊢\phi \to F:\mathrm{dom}F⟶𝒫V\setminus \left\{\varnothing \right\}$$
21	12 20 7	fun2d	$$⊢\phi \to \left(E\cup F\right):\mathrm{dom}E\cup \mathrm{dom}F⟶𝒫V\setminus \left\{\varnothing \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	difeq1d	$$⊢\phi \to 𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \right\}=𝒫V\setminus \left\{\varnothing \right\}$$
27	10 24 26	feq123d	$$⊢\phi \to \left(\mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \right\}\leftrightarrow \left(E\cup F\right):\mathrm{dom}E\cup \mathrm{dom}F⟶𝒫V\setminus \left\{\varnothing \right\}\right)$$
28	21 27	mpbird	$$⊢\phi \to \mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \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	isuhgr	$$⊢U\in W\to \left(U\in \mathrm{UHGraph}\leftrightarrow \mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \right\}\right)$$
32	8 31	syl	$$⊢\phi \to \left(U\in \mathrm{UHGraph}\leftrightarrow \mathrm{iEdg}\left(U\right):\mathrm{dom}\mathrm{iEdg}\left(U\right)⟶𝒫\mathrm{Vtx}\left(U\right)\setminus \left\{\varnothing \right\}\right)$$
33	28 32	mpbird	$$⊢\phi \to U\in \mathrm{UHGraph}$$