df-cup

Description: Define the little cup function. See brcup for its value. (Contributed by Scott Fenton, 14-Apr-2014)

		Ref	Expression
	Assertion	df-cup	$⊢ 𝖢𝗎𝗉 = ((V \times V) \times V) ∖ ran ((V \otimes E) ∆ ((({1^{st}}^{-1} \circ E) \cup ({2^{nd}}^{-1} \circ E)) \otimes V))$

Step	Hyp	Ref	Expression
0		ccup	$class 𝖢𝗎𝗉$
1		cvv	$class V$
2	1 1	cxp	$class (V \times V)$
3	2 1	cxp	$class ((V \times V) \times V)$
4		cep	$class E$
5	1 4	ctxp	$class (V \otimes E)$
6		c1st	$class 1^{st}$
7	6	ccnv	$class {1^{st}}^{-1}$
8	7 4	ccom	$class ({1^{st}}^{-1} \circ E)$
9		c2nd	$class 2^{nd}$
10	9	ccnv	$class {2^{nd}}^{-1}$
11	10 4	ccom	$class ({2^{nd}}^{-1} \circ E)$
12	8 11	cun	$class (({1^{st}}^{-1} \circ E) \cup ({2^{nd}}^{-1} \circ E))$
13	12 1	ctxp	$class ((({1^{st}}^{-1} \circ E) \cup ({2^{nd}}^{-1} \circ E)) \otimes V)$
14	5 13	csymdif	$class ((V \otimes E) ∆ ((({1^{st}}^{-1} \circ E) \cup ({2^{nd}}^{-1} \circ E)) \otimes V))$
15	14	crn	$class ran ((V \otimes E) ∆ ((({1^{st}}^{-1} \circ E) \cup ({2^{nd}}^{-1} \circ E)) \otimes V))$
16	3 15	cdif	$class (((V \times V) \times V) ∖ ran ((V \otimes E) ∆ ((({1^{st}}^{-1} \circ E) \cup ({2^{nd}}^{-1} \circ E)) \otimes V)))$
17	0 16	wceq	$wff 𝖢𝗎𝗉 = ((V \times V) \times V) ∖ ran ((V \otimes E) ∆ ((({1^{st}}^{-1} \circ E) \cup ({2^{nd}}^{-1} \circ E)) \otimes V))$

Metamath Proof Explorer