Metamath Proof Explorer

Definition df-apply

Description: Define the application function. See brapply for its value. (Contributed by Scott Fenton, 12-Apr-2014)

Ref Expression
Assertion df-apply 
|- Apply = ( ( Bigcup o. Bigcup ) o. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( ( Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 capply 
 |-  Apply
1 cbigcup 
 |-  Bigcup
2 1 1 ccom 
 |-  ( Bigcup o. Bigcup )
3 cvv 
 |-  _V
4 3 3 cxp 
 |-  ( _V X. _V )
5 cep 
 |-  _E
6 3 5 ctxp 
 |-  ( _V (x) _E )
7 csingles 
 |-  Singletons
8 5 7 cres 
 |-  ( _E |` Singletons )
9 8 3 ctxp 
 |-  ( ( _E |` Singletons ) (x) _V )
10 6 9 csymdif 
 |-  ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) )
11 10 crn 
 |-  ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) )
12 4 11 cdif 
 |-  ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) )
13 csingle 
 |-  Singleton
14 cimg 
 |-  Img
15 13 14 ccom 
 |-  ( Singleton o. Img )
16 cid 
 |-  _I
17 16 13 cpprod 
 |-  pprod ( _I , Singleton )
18 15 17 ccom 
 |-  ( ( Singleton o. Img ) o. pprod ( _I , Singleton ) )
19 12 18 ccom 
 |-  ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( ( Singleton o. Img ) o. pprod ( _I , Singleton ) ) )
20 2 19 ccom 
 |-  ( ( Bigcup o. Bigcup ) o. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( ( Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) )
21 0 20 wceq 
 |-  Apply = ( ( Bigcup o. Bigcup ) o. ( ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E |` Singletons ) (x) _V ) ) ) o. ( ( Singleton o. Img ) o. pprod ( _I , Singleton ) ) ) )