This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relbigcup

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

Ref Expression
Assertion relbigcup ⊢ Rel ⁡ 𝖡𝗂𝗀𝖼𝗎𝗉

Proof

Step Hyp Ref Expression
1 relxp ⊢ Rel ⁡ V × V
2 reldif ⊢ Rel ⁡ V × V → Rel ⁡ V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ E ⊗ V
3 1 2 ax-mp ⊢ Rel ⁡ V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ E ⊗ V
4 df-bigcup ⊢ 𝖡𝗂𝗀𝖼𝗎𝗉 = V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ E ⊗ V
5 4 releqi ⊢ Rel ⁡ 𝖡𝗂𝗀𝖼𝗎𝗉 ↔ Rel ⁡ V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ E ⊗ V
6 3 5 mpbir ⊢ Rel ⁡ 𝖡𝗂𝗀𝖼𝗎𝗉