Metamath Proof Explorer

Definition df-bigcup

Description: Define the Bigcup function, which, per fvbigcup , carries a set to its union. (Contributed by Scott Fenton, 11-Apr-2012)

Ref Expression
Assertion df-bigcup ⊢ 𝖡𝗂𝗀𝖼𝗎𝗉 = V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ E ⊗ V

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbigcup class 𝖡𝗂𝗀𝖼𝗎𝗉
1 cvv class V
2 1 1 cxp class V × V
3 cep class E
4 1 3 ctxp class V ⊗ E
5 3 3 ccom class E ∘ E
6 5 1 ctxp class E ∘ E ⊗ V
7 4 6 csymdif class V ⊗ E ∆ E ∘ E ⊗ V
8 7 crn class ran ⁡ V ⊗ E ∆ E ∘ E ⊗ V
9 2 8 cdif class V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ E ⊗ V
10 0 9 wceq wff 𝖡𝗂𝗀𝖼𝗎𝗉 = V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ E ⊗ V