P. 169 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16801-16900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	funcsetcestrclem7 16801*	Lemma 7 for funcsetcestrc 16804. (Contributed by AV, 27-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ( ph /\ X e. C ) -> ( ( X G X ) ` ( ( Id ` S ) ` X ) ) = ( ( Id ` E ) ` ( F ` X ) ) )
Theorem	funcsetcestrclem8 16802*	Lemma 8 for funcsetcestrc 16804. (Contributed by AV, 28-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X G Y ) : ( X ( Hom ` S ) Y ) --> ( ( F ` X ) ( Hom ` E ) ( F ` Y ) ) )
Theorem	funcsetcestrclem9 16803*	Lemma 9 for funcsetcestrc 16804. (Contributed by AV, 28-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) /\ ( H e. ( X ( Hom ` S ) Y ) /\ K e. ( Y ( Hom ` S ) Z ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. (comp ` S ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. (comp ` E ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )
Theorem	funcsetcestrc 16804*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 28-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ph -> F ( S Func E ) G )
Theorem	fthsetcestrc 16805*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is faithful. (Contributed by AV, 31-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ph -> F ( S Faith E ) G )
Theorem	fullsetcestrc 16806*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is full. (Contributed by AV, 1-Apr-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ph -> F ( S Full E ) G )
Theorem	embedsetcestrc 16807*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is an embedding. According to definition 3.27 (1) of [Adamek] p. 34, a functor "F is called an embedding provided that F is injective on morphisms", or according to remark 3.28 (1) in [Adamek] p. 34, "a functor is an embedding if and only if it is faithful and injective on objects". (Contributed by AV, 31-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   &    |- B = ( Base ` E )   =>    |- ( ph -> ( F ( S Faith E ) G /\ F : C -1-1-> B ) )
8.4  Categorical constructions
8.4.1  Product of categories
Syntax	cxpc 16808	Extend class notation with the product of two categories.
class X.c
Syntax	c1stf 16809	Extend class notation with the first projection functor.
class 1stF
Syntax	c2ndf 16810	Extend class notation with the second projection functor.
class 2ndF
Syntax	cprf 16811	Extend class notation with the functor pairing operation.
class ⟨,⟩F
Definition	df-xpc 16812*	Define the binary product of categories, which has objects for each pair of objects of the factors, and morphisms for each pair of morphisms of the factors. Composition is componentwise. (Contributed by Mario Carneiro, 10-Jan-2017.)
|- X.c = ( r e. _V , s e. _V |-> [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ [_ ( u e. b , v e. b |-> ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. (comp ` ndx ) , ( x e. ( b X. b ) , y e. b |-> ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. (comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. (comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } )
Definition	df-1stf 16813*	Define the first projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- 1stF = ( r e. Cat , s e. Cat |-> [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r X.c s ) ) y ) ) ) >. )
Definition	df-2ndf 16814*	Define the second projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- 2ndF = ( r e. Cat , s e. Cat |-> [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ <. ( 2nd |` b ) , ( x e. b , y e. b |-> ( 2nd |` ( x ( Hom ` ( r X.c s ) ) y ) ) ) >. )
Definition	df-prf 16815*	Define the pairing operation for functors (which takes two functors F : C --> D and G : C --> E and produces ( F ⟨,⟩F G ) : C --> ( D X.c E )). (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ⟨,⟩F = ( f e. _V , g e. _V |-> [_ dom ( 1st ` f ) / b ]_ <. ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ) , ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) ) >. )
Theorem	fnxpc 16816	The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.)
|- X.c Fn ( _V X. _V )
Theorem	xpcval 16817*	Value of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.)
|- T = ( C X.c D )   &    |- X = ( Base ` C )   &    |- Y = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- .x. = (comp ` C )   &    |- .xb = (comp ` D )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. W )   &    |- ( ph -> B = ( X X. Y ) )   &    |- ( ph -> K = ( u e. B , v e. B |-> ( ( ( 1st ` u ) H ( 1st ` v ) ) X. ( ( 2nd ` u ) J ( 2nd ` v ) ) ) ) )   &    |- ( ph -> O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) )   =>    |- ( ph -> T = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. (comp ` ndx ) , O >. } )
Theorem	xpcbas 16818	Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017.)
|- T = ( C X.c D )   &    |- X = ( Base ` C )   &    |- Y = ( Base ` D )   =>    |- ( X X. Y ) = ( Base ` T )
Theorem	xpchomfval 16819*	Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- K = ( Hom ` T )   =>    |- K = ( u e. B , v e. B |-> ( ( ( 1st ` u ) H ( 1st ` v ) ) X. ( ( 2nd ` u ) J ( 2nd ` v ) ) ) )
Theorem	xpchom 16820	Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- K = ( Hom ` T )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X K Y ) = ( ( ( 1st ` X ) H ( 1st ` Y ) ) X. ( ( 2nd ` X ) J ( 2nd ` Y ) ) ) )
Theorem	relxpchom 16821	A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- K = ( Hom ` T )   =>    |- Rel ( X K Y )
Theorem	xpccofval 16822*	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- K = ( Hom ` T )   &    |- .x. = (comp ` C )   &    |- .xb = (comp ` D )   &    |- O = (comp ` T )   =>    |- O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) )
Theorem	xpcco 16823	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- K = ( Hom ` T )   &    |- .x. = (comp ` C )   &    |- .xb = (comp ` D )   &    |- O = (comp ` T )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X K Y ) )   &    |- ( ph -> G e. ( Y K Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. O Z ) F ) = <. ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) , ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .xb ( 2nd ` Z ) ) ( 2nd ` F ) ) >. )
Theorem	xpcco1st 16824	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- K = ( Hom ` T )   &    |- O = (comp ` T )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X K Y ) )   &    |- ( ph -> G e. ( Y K Z ) )   &    |- .x. = (comp ` C )   =>    |- ( ph -> ( 1st ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 1st ` G ) ( <. ( 1st ` X ) , ( 1st ` Y ) >. .x. ( 1st ` Z ) ) ( 1st ` F ) ) )
Theorem	xpcco2nd 16825	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- K = ( Hom ` T )   &    |- O = (comp ` T )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X K Y ) )   &    |- ( ph -> G e. ( Y K Z ) )   &    |- .x. = (comp ` D )   =>    |- ( ph -> ( 2nd ` ( G ( <. X , Y >. O Z ) F ) ) = ( ( 2nd ` G ) ( <. ( 2nd ` X ) , ( 2nd ` Y ) >. .x. ( 2nd ` Z ) ) ( 2nd ` F ) ) )
Theorem	xpchom2 16826	Value of the set of morphisms in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- X = ( Base ` C )   &    |- Y = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- ( ph -> M e. X )   &    |- ( ph -> N e. Y )   &    |- ( ph -> P e. X )   &    |- ( ph -> Q e. Y )   &    |- K = ( Hom ` T )   =>    |- ( ph -> ( <. M , N >. K <. P , Q >. ) = ( ( M H P ) X. ( N J Q ) ) )
Theorem	xpcco2 16827	Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- X = ( Base ` C )   &    |- Y = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- ( ph -> M e. X )   &    |- ( ph -> N e. Y )   &    |- ( ph -> P e. X )   &    |- ( ph -> Q e. Y )   &    |- .x. = (comp ` C )   &    |- .xb = (comp ` D )   &    |- O = (comp ` T )   &    |- ( ph -> R e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> F e. ( M H P ) )   &    |- ( ph -> G e. ( N J Q ) )   &    |- ( ph -> K e. ( P H R ) )   &    |- ( ph -> L e. ( Q J S ) )   =>    |- ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) = <. ( K ( <. M , P >. .x. R ) F ) , ( L ( <. N , Q >. .xb S ) G ) >. )
Theorem	xpccatid 16828*	The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- X = ( Base ` C )   &    |- Y = ( Base ` D )   &    |- I = ( Id ` C )   &    |- J = ( Id ` D )   =>    |- ( ph -> ( T e. Cat /\ ( Id ` T ) = ( x e. X , y e. Y |-> <. ( I ` x ) , ( J ` y ) >. ) ) )
Theorem	xpcid 16829	The identity morphism in the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- X = ( Base ` C )   &    |- Y = ( Base ` D )   &    |- I = ( Id ` C )   &    |- J = ( Id ` D )   &    |- .1. = ( Id ` T )   &    |- ( ph -> R e. X )   &    |- ( ph -> S e. Y )   =>    |- ( ph -> ( .1. ` <. R , S >. ) = <. ( I ` R ) , ( J ` S ) >. )
Theorem	xpccat 16830	The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> T e. Cat )
Theorem	1stfval 16831*	Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- H = ( Hom ` T )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- P = ( C 1stF D )   =>    |- ( ph -> P = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. )
Theorem	1stf1 16832	Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- H = ( Hom ` T )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- P = ( C 1stF D )   &    |- ( ph -> R e. B )   =>    |- ( ph -> ( ( 1st ` P ) ` R ) = ( 1st ` R ) )
Theorem	1stf2 16833	Value of the first projection on a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- H = ( Hom ` T )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- P = ( C 1stF D )   &    |- ( ph -> R e. B )   &    |- ( ph -> S e. B )   =>    |- ( ph -> ( R ( 2nd ` P ) S ) = ( 1st |` ( R H S ) ) )
Theorem	2ndfval 16834*	Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- H = ( Hom ` T )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- Q = ( C 2ndF D )   =>    |- ( ph -> Q = <. ( 2nd |` B ) , ( x e. B , y e. B |-> ( 2nd |` ( x H y ) ) ) >. )
Theorem	2ndf1 16835	Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- H = ( Hom ` T )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- Q = ( C 2ndF D )   &    |- ( ph -> R e. B )   =>    |- ( ph -> ( ( 1st ` Q ) ` R ) = ( 2nd ` R ) )
Theorem	2ndf2 16836	Value of the first projection on a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- B = ( Base ` T )   &    |- H = ( Hom ` T )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- Q = ( C 2ndF D )   &    |- ( ph -> R e. B )   &    |- ( ph -> S e. B )   =>    |- ( ph -> ( R ( 2nd ` Q ) S ) = ( 2nd |` ( R H S ) ) )
Theorem	1stfcl 16837	The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- P = ( C 1stF D )   =>    |- ( ph -> P e. ( T Func C ) )
Theorem	2ndfcl 16838	The second projection functor is a functor onto the right argument. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- T = ( C X.c D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- Q = ( C 2ndF D )   =>    |- ( ph -> Q e. ( T Func D ) )
Theorem	prfval 16839*	Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- P = ( F ⟨,⟩F G )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func E ) )   =>    |- ( ph -> P = <. ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. )
Theorem	prf1 16840	Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- P = ( F ⟨,⟩F G )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func E ) )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( 1st ` P ) ` X ) = <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. )
Theorem	prf2fval 16841*	Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- P = ( F ⟨,⟩F G )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func E ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( 2nd ` P ) Y ) = ( h e. ( X H Y ) |-> <. ( ( X ( 2nd ` F ) Y ) ` h ) , ( ( X ( 2nd ` G ) Y ) ` h ) >. ) )
Theorem	prf2 16842	Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- P = ( F ⟨,⟩F G )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func E ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> K e. ( X H Y ) )   =>    |- ( ph -> ( ( X ( 2nd ` P ) Y ) ` K ) = <. ( ( X ( 2nd ` F ) Y ) ` K ) , ( ( X ( 2nd ` G ) Y ) ` K ) >. )
Theorem	prfcl 16843	The pairing of functors F : C --> D and G : C --> D is a functor <. F , G >. : C --> ( D X. E ). (Contributed by Mario Carneiro, 12-Jan-2017.)
|- P = ( F ⟨,⟩F G )   &    |- T = ( D X.c E )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func E ) )   =>    |- ( ph -> P e. ( C Func T ) )
Theorem	prf1st 16844	Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- P = ( F ⟨,⟩F G )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func E ) )   =>    |- ( ph -> ( ( D 1stF E ) o.func P ) = F )
Theorem	prf2nd 16845	Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- P = ( F ⟨,⟩F G )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func E ) )   =>    |- ( ph -> ( ( D 2ndF E ) o.func P ) = G )
Theorem	1st2ndprf 16846	Break a functor into a product category into first and second projections. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- T = ( D X.c E )   &    |- ( ph -> F e. ( C Func T ) )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   =>    |- ( ph -> F = ( ( ( D 1stF E ) o.func F ) ⟨,⟩F ( ( D 2ndF E ) o.func F ) ) )
Theorem	catcxpccl 16847	The category of categories for a weak universe is closed under the product category operation. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- T = ( X X.c Y )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> T e. B )
Theorem	xpcpropd 16848	If two categories have the same set of objects, morphisms, and compositions, then they have the same product category. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- ( ph -> ( Hom f ` A ) = ( Hom f ` B ) )   &    |- ( ph -> (compf ` A ) = (compf ` B ) )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( A X.c C ) = ( B X.c D ) )
8.4.2  Functor evaluation
Syntax	cevlf 16849	Extend class notation with the evaluation functor.
class evalF
Syntax	ccurf 16850	Extend class notation with the currying of a functor.
class curryF
Syntax	cuncf 16851	Extend class notation with the uncurrying of a functor.
class uncurryF
Syntax	cdiag 16852	Extend class notation to include the diagonal functor.
class Δfunc
Definition	df-evlf 16853*	Define the evaluation functor, which is the extension of the evaluation map f , x |-> ( f ` x ) of functors, to a functor ( C --> D ) X. C --> D. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- evalF = ( c e. Cat , d e. Cat |-> <. ( f e. ( c Func d ) , x e. ( Base ` c ) |-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( c Func d ) X. ( Base ` c ) ) , y e. ( ( c Func d ) X. ( Base ` c ) ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( c Nat d ) n ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. (comp ` d ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. )
Definition	df-curf 16854*	Define the curry functor, which maps a functor F : C X. D --> E to curryF ( F ) : C --> ( D --> E ). (Contributed by Mario Carneiro, 11-Jan-2017.)
|- curryF = ( e e. _V , f e. _V |-> [_ ( 1st ` e ) / c ]_ [_ ( 2nd ` e ) / d ]_ <. ( x e. ( Base ` c ) |-> <. ( y e. ( Base ` d ) |-> ( x ( 1st ` f ) y ) ) , ( y e. ( Base ` d ) , z e. ( Base ` d ) |-> ( g e. ( y ( Hom ` d ) z ) |-> ( ( ( Id ` c ) ` x ) ( <. x , y >. ( 2nd ` f ) <. x , z >. ) g ) ) ) >. ) , ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( g e. ( x ( Hom ` c ) y ) |-> ( z e. ( Base ` d ) |-> ( g ( <. x , z >. ( 2nd ` f ) <. y , z >. ) ( ( Id ` d ) ` z ) ) ) ) ) >. )
Definition	df-uncf 16855*	Define the uncurry functor, which can be defined equationally using evalF. Strictly speaking, the third category argument is not needed, since the resulting functor is extensionally equal regardless, but it is used in the equational definition and is too much work to remove. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- uncurryF = ( c e. _V , f e. _V |-> ( ( ( c ` 1 ) evalF ( c ` 2 ) ) o.func ( ( f o.func ( ( c ` 0 ) 1stF ( c ` 1 ) ) ) ⟨,⟩F ( ( c ` 0 ) 2ndF ( c ` 1 ) ) ) ) )
Definition	df-diag 16856*	Define the diagonal functor, which is the functor C --> ( D Func C ) whose object part is x e. C |-> ( y e. D |-> x ). The value of the functor at an object x is the constant functor which maps all objects in D to x and all morphisms to 1 ( x ). The morphism part is a natural transformation between these functors, which takes f : x --> y to the natural transformation with every component equal to f. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Δfunc = ( c e. Cat , d e. Cat |-> ( <. c , d >. curryF ( c 1stF d ) ) )
Theorem	evlfval 16857*	Value of the evaluation functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- E = ( C evalF D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` D )   &    |- N = ( C Nat D )   =>    |- ( ph -> E = <. ( f e. ( C Func D ) , x e. B |-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m N n ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. .x. ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. )
Theorem	evlf2 16858*	Value of the evaluation functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- E = ( C evalF D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` D )   &    |- N = ( C Nat D )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func D ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- L = ( <. F , X >. ( 2nd ` E ) <. G , Y >. )   =>    |- ( ph -> L = ( a e. ( F N G ) , g e. ( X H Y ) |-> ( ( a ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` g ) ) ) )
Theorem	evlf2val 16859	Value of the evaluation natural transformation at an object. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- E = ( C evalF D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` D )   &    |- N = ( C Nat D )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func D ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- L = ( <. F , X >. ( 2nd ` E ) <. G , Y >. )   &    |- ( ph -> A e. ( F N G ) )   &    |- ( ph -> K e. ( X H Y ) )   =>    |- ( ph -> ( A L K ) = ( ( A ` Y ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` Y ) >. .x. ( ( 1st ` G ) ` Y ) ) ( ( X ( 2nd ` F ) Y ) ` K ) ) )
Theorem	evlf1 16860	Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- E = ( C evalF D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( F ( 1st ` E ) X ) = ( ( 1st ` F ) ` X ) )
Theorem	evlfcllem 16861	Lemma for evlfcl 16862. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- E = ( C evalF D )   &    |- Q = ( C FuncCat D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- N = ( C Nat D )   &    |- ( ph -> ( F e. ( C Func D ) /\ X e. ( Base ` C ) ) )   &    |- ( ph -> ( G e. ( C Func D ) /\ Y e. ( Base ` C ) ) )   &    |- ( ph -> ( H e. ( C Func D ) /\ Z e. ( Base ` C ) ) )   &    |- ( ph -> ( A e. ( F N G ) /\ K e. ( X ( Hom ` C ) Y ) ) )   &    |- ( ph -> ( B e. ( G N H ) /\ L e. ( Y ( Hom ` C ) Z ) ) )   =>    |- ( ph -> ( ( <. F , X >. ( 2nd ` E ) <. H , Z >. ) ` ( <. B , L >. ( <. <. F , X >. , <. G , Y >. >. (comp ` ( Q X.c C ) ) <. H , Z >. ) <. A , K >. ) ) = ( ( ( <. G , Y >. ( 2nd ` E ) <. H , Z >. ) ` <. B , L >. ) ( <. ( ( 1st ` E ) ` <. F , X >. ) , ( ( 1st ` E ) ` <. G , Y >. ) >. (comp ` D ) ( ( 1st ` E ) ` <. H , Z >. ) ) ( ( <. F , X >. ( 2nd ` E ) <. G , Y >. ) ` <. A , K >. ) ) )
Theorem	evlfcl 16862	The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors C --> D, and the second parameter in D. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- E = ( C evalF D )   &    |- Q = ( C FuncCat D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> E e. ( ( Q X.c C ) Func D ) )
Theorem	curfval 16863*	Value of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- J = ( Hom ` D )   &    |- .1. = ( Id ` C )   &    |- H = ( Hom ` C )   &    |- I = ( Id ` D )   =>    |- ( ph -> G = <. ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) , ( x e. A , y e. A |-> ( g e. ( x H y ) |-> ( z e. B |-> ( g ( <. x , z >. ( 2nd ` F ) <. y , z >. ) ( I ` z ) ) ) ) ) >. )
Theorem	curf1fval 16864*	Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- J = ( Hom ` D )   &    |- .1. = ( Id ` C )   =>    |- ( ph -> ( 1st ` G ) = ( x e. A |-> <. ( y e. B |-> ( x ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` x ) ( <. x , y >. ( 2nd ` F ) <. x , z >. ) g ) ) ) >. ) )
Theorem	curf1 16865*	Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- ( ph -> X e. A )   &    |- K = ( ( 1st ` G ) ` X )   &    |- J = ( Hom ` D )   &    |- .1. = ( Id ` C )   =>    |- ( ph -> K = <. ( y e. B |-> ( X ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y J z ) |-> ( ( .1. ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) >. )
Theorem	curf11 16866	Value of the double evaluated curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- ( ph -> X e. A )   &    |- K = ( ( 1st ` G ) ` X )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( 1st ` K ) ` Y ) = ( X ( 1st ` F ) Y ) )
Theorem	curf12 16867	The partially evaluated curry functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- ( ph -> X e. A )   &    |- K = ( ( 1st ` G ) ` X )   &    |- ( ph -> Y e. B )   &    |- J = ( Hom ` D )   &    |- .1. = ( Id ` C )   &    |- ( ph -> Z e. B )   &    |- ( ph -> H e. ( Y J Z ) )   =>    |- ( ph -> ( ( Y ( 2nd ` K ) Z ) ` H ) = ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` F ) <. X , Z >. ) H ) )
Theorem	curf1cl 16868	The partially evaluated curry functor is a functor. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- ( ph -> X e. A )   &    |- K = ( ( 1st ` G ) ` X )   =>    |- ( ph -> K e. ( D Func E ) )
Theorem	curf2 16869*	Value of the curry functor at a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- I = ( Id ` D )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> K e. ( X H Y ) )   &    |- L = ( ( X ( 2nd ` G ) Y ) ` K )   =>    |- ( ph -> L = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) )
Theorem	curf2val 16870	Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- I = ( Id ` D )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> K e. ( X H Y ) )   &    |- L = ( ( X ( 2nd ` G ) Y ) ` K )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( L ` Z ) = ( K ( <. X , Z >. ( 2nd ` F ) <. Y , Z >. ) ( I ` Z ) ) )
Theorem	curf2cl 16871	The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- I = ( Id ` D )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> K e. ( X H Y ) )   &    |- L = ( ( X ( 2nd ` G ) Y ) ` K )   &    |- N = ( D Nat E )   =>    |- ( ph -> L e. ( ( ( 1st ` G ) ` X ) N ( ( 1st ` G ) ` Y ) ) )
Theorem	curfcl 16872	The curry functor of a functor F : C X. D --> E is a functor curryF ( F ) : C --> ( D --> E ). (Contributed by Mario Carneiro, 13-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- Q = ( D FuncCat E )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   =>    |- ( ph -> G e. ( C Func Q ) )
Theorem	curfpropd 16873	If two categories have the same set of objects, morphisms, and compositions, then they curry the same functor to the same result. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> ( Hom f ` A ) = ( Hom f ` B ) )   &    |- ( ph -> (compf ` A ) = (compf ` B ) )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> A e. Cat )   &    |- ( ph -> B e. Cat )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( A X.c C ) Func E ) )   =>    |- ( ph -> ( <. A , C >. curryF F ) = ( <. B , D >. curryF F ) )
Theorem	uncfval 16874	Value of the uncurry functor, which is the reverse of the curry functor, taking G : C --> ( D --> E ) to uncurryF ( G ) : C X. D --> E. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- F = ( <" C D E "> uncurryF G )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )   =>    |- ( ph -> F = ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) ⟨,⟩F ( C 2ndF D ) ) ) )
Theorem	uncfcl 16875	The uncurry operation takes a functor F : C --> ( D --> E ) to a functor uncurryF ( F ) : C X. D --> E. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- F = ( <" C D E "> uncurryF G )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )   =>    |- ( ph -> F e. ( ( C X.c D ) Func E ) )
Theorem	uncf1 16876	Value of the uncurry functor on an object. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- F = ( <" C D E "> uncurryF G )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )   &    |- A = ( Base ` C )   &    |- B = ( Base ` D )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( 1st ` F ) Y ) = ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) )
Theorem	uncf2 16877	Value of the uncurry functor on a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- F = ( <" C D E "> uncurryF G )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )   &    |- A = ( Base ` C )   &    |- B = ( Base ` D )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. B )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- ( ph -> Z e. A )   &    |- ( ph -> W e. B )   &    |- ( ph -> R e. ( X H Z ) )   &    |- ( ph -> S e. ( Y J W ) )   =>    |- ( ph -> ( R ( <. X , Y >. ( 2nd ` F ) <. Z , W >. ) S ) = ( ( ( ( X ( 2nd ` G ) Z ) ` R ) ` W ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` W ) >. (comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Z ) ) ` W ) ) ( ( Y ( 2nd ` ( ( 1st ` G ) ` X ) ) W ) ` S ) ) )
Theorem	curfuncf 16878	Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- F = ( <" C D E "> uncurryF G )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )   =>    |- ( ph -> ( <. C , D >. curryF F ) = G )
Theorem	uncfcurf 16879	Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   =>    |- ( ph -> ( <" C D E "> uncurryF G ) = F )
Theorem	diagval 16880	Define the diagonal functor, which is the functor C --> ( D Func C ) whose object part is x e. C |-> ( y e. D |-> x ). We can define this equationally as the currying of the first projection functor, and by expressing it this way we get a quick proof of functoriality. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
|- L = ( CΔfunc D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> L = ( <. C , D >. curryF ( C 1stF D ) ) )
Theorem	diagcl 16881	The diagonal functor is a functor from the base category to the functor category. Another way of saying this is that the constant functor ( y e. D |-> X ) is a construction that is natural in X (and covariant). (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
|- L = ( CΔfunc D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- Q = ( D FuncCat C )   =>    |- ( ph -> L e. ( C Func Q ) )
Theorem	diag1cl 16882	The constant functor of X is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
|- L = ( CΔfunc D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- A = ( Base ` C )   &    |- ( ph -> X e. A )   &    |- K = ( ( 1st ` L ) ` X )   =>    |- ( ph -> K e. ( D Func C ) )
Theorem	diag11 16883	Value of the constant functor at an object. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
|- L = ( CΔfunc D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- A = ( Base ` C )   &    |- ( ph -> X e. A )   &    |- K = ( ( 1st ` L ) ` X )   &    |- B = ( Base ` D )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( 1st ` K ) ` Y ) = X )
Theorem	diag12 16884	Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
|- L = ( CΔfunc D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- A = ( Base ` C )   &    |- ( ph -> X e. A )   &    |- K = ( ( 1st ` L ) ` X )   &    |- B = ( Base ` D )   &    |- ( ph -> Y e. B )   &    |- J = ( Hom ` D )   &    |- .1. = ( Id ` C )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( Y J Z ) )   =>    |- ( ph -> ( ( Y ( 2nd ` K ) Z ) ` F ) = ( .1. ` X ) )
Theorem	diag2 16885	Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- L = ( CΔfunc D )   &    |- A = ( Base ` C )   &    |- B = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) = ( B X. { F } ) )
Theorem	diag2cl 16886	The diagonal functor at a morphism is a natural transformation between constant functors. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- L = ( CΔfunc D )   &    |- A = ( Base ` C )   &    |- B = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> F e. ( X H Y ) )   &    |- N = ( D Nat C )   =>    |- ( ph -> ( B X. { F } ) e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
Theorem	curf2ndf 16887	As shown in diagval 16880, the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is x e. C |-> ( y e. D |-> y ), which is a constant functor of the identity functor at D. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- Q = ( D FuncCat D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> ( <. C , D >. curryF ( C 2ndF D ) ) = ( ( 1st ` ( QΔfunc C ) ) ` (idfunc ` D ) ) )
8.4.3  Hom functor
Syntax	chof 16888	Extend class notation with the Hom functor.
class HomF
Syntax	cyon 16889	Extend class notation with the Yoneda embedding.
class Yon
Definition	df-hof 16890*	Define the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat ` C ) X. C to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- HomF = ( c e. Cat |-> <. ( Hom f ` c ) , [_ ( Base ` c ) / b ]_ ( x e. ( b X. b ) , y e. ( b X. b ) |-> ( f e. ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x (comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. (comp ` c ) ( 2nd ` y ) ) f ) ) ) ) >. )
Definition	df-yon 16891	Define the Yoneda embedding, which is the currying of the (opposite) Hom functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- Yon = ( c e. Cat |-> ( <. c , (oppCat ` c ) >. curryF (HomF ` (oppCat ` c ) ) ) )
Theorem	hofval 16892*	Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat ` C ) X. C to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   =>    |- ( ph -> M = <. ( Hom f ` C ) , ( x e. ( B X. B ) , y e. ( B X. B ) |-> ( f e. ( ( 1st ` y ) H ( 1st ` x ) ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( h e. ( H ` x ) |-> ( ( g ( x .x. ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. .x. ( 2nd ` y ) ) f ) ) ) ) >. )
Theorem	hof1fval 16893	The object part of the Hom functor is the Hom f operation, which is just a functionalized version of Hom. That is, it is a two argument function, which maps X , Y to the set of morphisms from X to Y. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   =>    |- ( ph -> ( 1st ` M ) = ( Hom f ` C ) )
Theorem	hof1 16894	The object part of the Hom functor maps X , Y to the set of morphisms from X to Y. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( 1st ` M ) Y ) = ( X H Y ) )
Theorem	hof2fval 16895*	The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W), yields a function (a morphism of SetCat) mapping h : X --> Y to g o. h o. f : Z --> W. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. B )   &    |- .x. = (comp ` C )   =>    |- ( ph -> ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) = ( f e. ( Z H X ) , g e. ( Y H W ) |-> ( h e. ( X H Y ) |-> ( ( g ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) f ) ) ) )
Theorem	hof2val 16896*	The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W), yields a function (a morphism of SetCat) mapping h : X --> Y to g o. h o. f : Z --> W. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. B )   &    |- .x. = (comp ` C )   &    |- ( ph -> F e. ( Z H X ) )   &    |- ( ph -> G e. ( Y H W ) )   =>    |- ( ph -> ( F ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) G ) = ( h e. ( X H Y ) |-> ( ( G ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) F ) ) )
Theorem	hof2 16897	The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W), yields a function (a morphism of SetCat) mapping h : X --> Y to g o. h o. f : Z --> W. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. B )   &    |- .x. = (comp ` C )   &    |- ( ph -> F e. ( Z H X ) )   &    |- ( ph -> G e. ( Y H W ) )   &    |- ( ph -> K e. ( X H Y ) )   =>    |- ( ph -> ( ( F ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) G ) ` K ) = ( ( G ( <. X , Y >. .x. W ) K ) ( <. Z , X >. .x. W ) F ) )
Theorem	hofcllem 16898	Lemma for hofcl 16899. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- O = (oppCat ` C )   &    |- D = ( SetCat ` U )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. B )   &    |- ( ph -> S e. B )   &    |- ( ph -> T e. B )   &    |- ( ph -> K e. ( Z H X ) )   &    |- ( ph -> L e. ( Y H W ) )   &    |- ( ph -> P e. ( S H Z ) )   &    |- ( ph -> Q e. ( W H T ) )   =>    |- ( ph -> ( ( K ( <. S , Z >. (comp ` C ) X ) P ) ( <. X , Y >. ( 2nd ` M ) <. S , T >. ) ( Q ( <. Y , W >. (comp ` C ) T ) L ) ) = ( ( P ( <. Z , W >. ( 2nd ` M ) <. S , T >. ) Q ) ( <. ( X H Y ) , ( Z H W ) >. (comp ` D ) ( S H T ) ) ( K ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) L ) ) )
Theorem	hofcl 16899	Closure of the Hom functor. Note that the codomain is the category SetCat ` U for any universe U which contains each Hom-set. This corresponds to the assertion that C be locally small (with respect to U). (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- O = (oppCat ` C )   &    |- D = ( SetCat ` U )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   =>    |- ( ph -> M e. ( ( O X.c C ) Func D ) )
Theorem	oppchofcl 16900	Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- O = (oppCat ` C )   &    |- M = (HomF ` O )   &    |- D = ( SetCat ` U )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   =>    |- ( ph -> M e. ( ( C X.c O ) Func D ) )