Metamath Proof Explorer


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 X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( ( `' 1st o. _E ) u. ( `' 2nd o. _E ) ) (x) _V ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccup
 |-  Cup
1 cvv
 |-  _V
2 1 1 cxp
 |-  ( _V X. _V )
3 2 1 cxp
 |-  ( ( _V X. _V ) X. _V )
4 cep
 |-  _E
5 1 4 ctxp
 |-  ( _V (x) _E )
6 c1st
 |-  1st
7 6 ccnv
 |-  `' 1st
8 7 4 ccom
 |-  ( `' 1st o. _E )
9 c2nd
 |-  2nd
10 9 ccnv
 |-  `' 2nd
11 10 4 ccom
 |-  ( `' 2nd o. _E )
12 8 11 cun
 |-  ( ( `' 1st o. _E ) u. ( `' 2nd o. _E ) )
13 12 1 ctxp
 |-  ( ( ( `' 1st o. _E ) u. ( `' 2nd o. _E ) ) (x) _V )
14 5 13 csymdif
 |-  ( ( _V (x) _E ) /_\ ( ( ( `' 1st o. _E ) u. ( `' 2nd o. _E ) ) (x) _V ) )
15 14 crn
 |-  ran ( ( _V (x) _E ) /_\ ( ( ( `' 1st o. _E ) u. ( `' 2nd o. _E ) ) (x) _V ) )
16 3 15 cdif
 |-  ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( ( `' 1st o. _E ) u. ( `' 2nd o. _E ) ) (x) _V ) ) )
17 0 16 wceq
 |-  Cup = ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( ( `' 1st o. _E ) u. ( `' 2nd o. _E ) ) (x) _V ) ) )