Definition 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	⊢ Cup = ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( ( ( ◡ 1st ∘ E ) ∪ ( ◡ 2nd ∘ E ) ) ⊗ V ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccup	⊢ Cup
1		cvv	⊢ V
2	1 1	cxp	⊢ ( V × V )
3	2 1	cxp	⊢ ( ( V × V ) × V )
4		cep	⊢ E
5	1 4	ctxp	⊢ ( V ⊗ E )
6		c1st	⊢ 1st
7	6	ccnv	⊢ ◡ 1st
8	7 4	ccom	⊢ ( ◡ 1st ∘ E )
9		c2nd	⊢ 2nd
10	9	ccnv	⊢ ◡ 2nd
11	10 4	ccom	⊢ ( ◡ 2nd ∘ E )
12	8 11	cun	⊢ ( ( ◡ 1st ∘ E ) ∪ ( ◡ 2nd ∘ E ) )
13	12 1	ctxp	⊢ ( ( ( ◡ 1st ∘ E ) ∪ ( ◡ 2nd ∘ E ) ) ⊗ V )
14	5 13	csymdif	⊢ ( ( V ⊗ E ) △ ( ( ( ◡ 1st ∘ E ) ∪ ( ◡ 2nd ∘ E ) ) ⊗ V ) )
15	14	crn	⊢ ran ( ( V ⊗ E ) △ ( ( ( ◡ 1st ∘ E ) ∪ ( ◡ 2nd ∘ E ) ) ⊗ V ) )
16	3 15	cdif	⊢ ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( ( ( ◡ 1st ∘ E ) ∪ ( ◡ 2nd ∘ E ) ) ⊗ V ) ) )
17	0 16	wceq	⊢ Cup = ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( ( ( ◡ 1st ∘ E ) ∪ ( ◡ 2nd ∘ E ) ) ⊗ V ) ) )