# Metamath Proof Explorer

## 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}×\mathrm{V}\right)$
2 reldif ${⊢}\mathrm{Rel}\left(\mathrm{V}×\mathrm{V}\right)\to \mathrm{Rel}\left(\left(\mathrm{V}×\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}×\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}×\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{𝖡𝗂𝗀𝖼𝗎𝗉}↔\mathrm{Rel}\left(\left(\mathrm{V}×\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{𝖡𝗂𝗀𝖼𝗎𝗉}$