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 ) ) )