Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-apply Structured version   Unicode version

Definition df-apply 25717
Description: Define the application function. See brapply 25783 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
Assertion
Ref Expression
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 of Definition df-apply
StepHypRef Expression
1 capply 25689 . 2  class Apply
2 cbigcup 25678 . . . 4  class  Bigcup
32, 2ccom 4882 . . 3  class  ( Bigcup  o. 
Bigcup )
4 cvv 2956 . . . . . 6  class  _V
54, 4cxp 4876 . . . . 5  class  ( _V 
X.  _V )
6 cep 4492 . . . . . . . 8  class  _E
74, 6ctxp 25674 . . . . . . 7  class  ( _V 
(x)  _E  )
8 csingles 25683 . . . . . . . . 9  class  Singletons
96, 8cres 4880 . . . . . . . 8  class  (  _E  |` 
Singletons )
109, 4ctxp 25674 . . . . . . 7  class  ( (  _E  |`  Singletons )  (x)  _V )
117, 10csymdif 25662 . . . . . 6  class  ( ( _V  (x)  _E  )(++) ( (  _E  |`  Singletons )  (x)  _V ) )
1211crn 4879 . . . . 5  class  ran  (
( _V  (x)  _E  )(++) ( (  _E  |`  Singletons )  (x)  _V ) )
135, 12cdif 3317 . . . 4  class  ( ( _V  X.  _V )  \  ran  ( ( _V 
(x)  _E  )(++) (
(  _E  |`  Singletons )  (x)  _V ) ) )
14 csingle 25682 . . . . . 6  class Singleton
15 cimg 25686 . . . . . 6  class Img
1614, 15ccom 4882 . . . . 5  class  (Singleton  o. Img )
17 cid 4493 . . . . . 6  class  _I
1817, 14cpprod 25675 . . . . 5  class pprod (  _I  , Singleton )
1916, 18ccom 4882 . . . 4  class  ( (Singleton  o. Img )  o. pprod (  _I  , Singleton ) )
2013, 19ccom 4882 . . 3  class  ( ( ( _V  X.  _V )  \  ran  ( ( _V  (x)  _E  )(++) ( (  _E  |`  Singletons )  (x)  _V ) ) )  o.  ( (Singleton  o. Img )  o. pprod (  _I  , Singleton ) ) )
213, 20ccom 4882 . 2  class  ( (
Bigcup  o.  Bigcup )  o.  (
( ( _V  X.  _V )  \  ran  (
( _V  (x)  _E  )(++) ( (  _E  |`  Singletons )  (x)  _V ) ) )  o.  ( (Singleton  o. Img )  o. pprod (  _I  , Singleton ) ) ) )
221, 21wceq 1652 1  wff Apply  =  ( ( Bigcup  o.  Bigcup )  o.  ( ( ( _V 
X.  _V )  \  ran  ( ( _V  (x)  _E  )(++) ( (  _E  |` 
Singletons )  (x)  _V )
) )  o.  (
(Singleton  o. Img )  o. pprod (  _I  , Singleton ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  brapply  25783
  Copyright terms: Public domain W3C validator