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 \times V) ∖ ran ((V \otimes E) ∆ ((E \circ E) \otimes V))$

Step	Hyp	Ref	Expression
0		cbigcup	$class 𝖡𝗂𝗀𝖼𝗎𝗉$
1		cvv	$class V$
2	1 1	cxp	$class (V \times V)$
3		cep	$class E$
4	1 3	ctxp	$class (V \otimes E)$
5	3 3	ccom	$class (E \circ E)$
6	5 1	ctxp	$class ((E \circ E) \otimes V)$
7	4 6	csymdif	$class ((V \otimes E) ∆ ((E \circ E) \otimes V))$
8	7	crn	$class ran ((V \otimes E) ∆ ((E \circ E) \otimes V))$
9	2 8	cdif	$class ((V \times V) ∖ ran ((V \otimes E) ∆ ((E \circ E) \otimes V)))$
10	0 9	wceq	$wff 𝖡𝗂𝗀𝖼𝗎𝗉 = (V \times V) ∖ ran ((V \otimes E) ∆ ((E \circ E) \otimes V))$

Metamath Proof Explorer