Theorem relbigcup

Description: The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Assertion	relbigcup	$$⊢\mathrm{Rel}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}$$

Proof

Step	Hyp	Ref	Expression
1		relxp	$$⊢\mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)$$
2		reldif	$$⊢\mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{Rel}\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\mathrm{E}\circ \mathrm{E}\right)\otimes \mathrm{V}\right)\right)\right)$$
3	1 2	ax-mp	$$⊢\mathrm{Rel}\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\mathrm{E}\circ \mathrm{E}\right)\otimes \mathrm{V}\right)\right)\right)$$
4		df-bigcup	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\mathrm{E}\circ \mathrm{E}\right)\otimes \mathrm{V}\right)\right)$$
5	4	releqi	$$⊢\mathrm{Rel}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\leftrightarrow \mathrm{Rel}\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\mathrm{E}\circ \mathrm{E}\right)\otimes \mathrm{V}\right)\right)\right)$$
6	3 5	mpbir	$$⊢\mathrm{Rel}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}$$