P. 158 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15701-15800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cicfval 15701	The set of isomorphic objects of the category c. (Contributed by AV, 4-Apr-2020.)
|- ( C e. Cat -> ( ~=c𝑐 ` C ) = ( ( Iso ` C ) supp (/) ) )
Theorem	brcic 15702	The relation "is isomorphic to" for categories. (Contributed by AV, 5-Apr-2020.)
|- I = ( Iso ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( ~=c𝑐 ` C ) Y <-> ( X I Y ) =/= (/) ) )
Theorem	cic 15703*	Objects X and Y in a category are isomorphic provided that there is an isomorphism f : X --> Y, see definition 3.15 of [Adamek] p. 29. (Contributed by AV, 4-Apr-2020.)
|- I = ( Iso ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( ~=c𝑐 ` C ) Y <-> E. f f e. ( X I Y ) ) )
Theorem	brcici 15704	Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020.)
|- I = ( Iso ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X I Y ) )   =>    |- ( ph -> X ( ~=c𝑐 ` C ) Y )
Theorem	cicref 15705	Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020.)
|- ( ( C e. Cat /\ O e. ( Base ` C ) ) -> O ( ~=c𝑐 ` C ) O )
Theorem	ciclcl 15706	Isomorphism implies the left side is an object. (Contributed by AV, 5-Apr-2020.)
|- ( ( C e. Cat /\ R ( ~=c𝑐 ` C ) S ) -> R e. ( Base ` C ) )
Theorem	cicrcl 15707	Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020.)
|- ( ( C e. Cat /\ R ( ~=c𝑐 ` C ) S ) -> S e. ( Base ` C ) )
Theorem	cicsym 15708	Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.)
|- ( ( C e. Cat /\ R ( ~=c𝑐 ` C ) S ) -> S ( ~=c𝑐 ` C ) R )
Theorem	cictr 15709	Isomorphism is transitive. (Contributed by AV, 5-Apr-2020.)
|- ( ( C e. Cat /\ R ( ~=c𝑐 ` C ) S /\ S ( ~=c𝑐 ` C ) T ) -> R ( ~=c𝑐 ` C ) T )
Theorem	cicer 15710	Isomorphism is an equivalence relation on objects of a category. Remark 3.16 in [Adamek] p. 29. (Contributed by AV, 5-Apr-2020.)
|- ( C e. Cat -> ( ~=c𝑐 ` C ) Er ( Base ` C ) )
8.1.6  Subcategories
Syntax	cssc 15711	Extend class notation to include the subset relation for subcategories.
class C_cat
Syntax	cresc 15712	Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms).
class |`cat
Syntax	csubc 15713	Extend class notation to include the collection of subcategories of a category.
class Subcat
Definition	df-ssc 15714*	Define the subset relation for subcategories. Despite the name, this is not really a "category-aware" definition, which is to say it makes no explicit references to homsets or composition; instead this is a subset-like relation on the functions that are used as subcategory specifications in df-subc 15716, which makes it play an analogous role to the subset relation applied to the subgroups of a group. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- C_cat = { <. h , j >. | E. t ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) ) }
Definition	df-resc 15715*	Define the restriction of a category to a given set of arrows. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- |`cat = ( c e. _V , h e. _V |-> ( ( c ↾s dom dom h ) sSet <. ( Hom ` ndx ) , h >. ) )
Definition	df-subc 15716*	(Subcat ` C ) is the set of all the subcategory specifications of the category C. Like df-subg 16813, this is not actually a collection of categories (as in definition 4.1(a) of [Adamek] p. 48), but only sets which when given operations from the base category (using df-resc 15715) form a category. All the objects and all the morphisms of the subcategory belong to the supercategory. The identity of an object, the domain and the codomain of a morphism are the same in the subcategory and the supercategory. The composition of the subcategory is a restriction of the composition of the supercategory. (Contributed by FL, 17-Sep-2009.) (Revised by Mario Carneiro, 4-Jan-2017.)
|- Subcat = ( c e. Cat |-> { h | ( h C_cat ( Hom f ` c ) /\ [. dom dom h / s ]. A. x e. s ( ( ( Id ` c ) ` x ) e. ( x h x ) /\ A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. (comp ` c ) z ) f ) e. ( x h z ) ) ) } )
Theorem	sscrel 15717	The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Rel C_cat
Theorem	brssc 15718*	The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( H C_cat J <-> E. t ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ x e. ( s X. s ) ~P ( J ` x ) ) )
Theorem	sscpwex 15719*	An analogue of pwex 4607 for the subcategory subset relation: The collection of subcategory subsets of a given set J is a set. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- { h | h C_cat J } e. _V
Theorem	subcrcl 15720	Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( H e. (Subcat ` C ) -> C e. Cat )
Theorem	sscfn1 15721	The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> H C_cat J )   &    |- ( ph -> S = dom dom H )   =>    |- ( ph -> H Fn ( S X. S ) )
Theorem	sscfn2 15722	The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> H C_cat J )   &    |- ( ph -> T = dom dom J )   =>    |- ( ph -> J Fn ( T X. T ) )
Theorem	ssclem 15723	Lemma for ssc1 15725 and similar theorems. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> H Fn ( S X. S ) )   =>    |- ( ph -> ( H e. _V <-> S e. _V ) )
Theorem	isssc 15724*	Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> H Fn ( S X. S ) )   &    |- ( ph -> J Fn ( T X. T ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( H C_cat J <-> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) )
Theorem	ssc1 15725	Infer subset relation on objects from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> H Fn ( S X. S ) )   &    |- ( ph -> J Fn ( T X. T ) )   &    |- ( ph -> H C_cat J )   =>    |- ( ph -> S C_ T )
Theorem	ssc2 15726	Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> H Fn ( S X. S ) )   &    |- ( ph -> H C_cat J )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   =>    |- ( ph -> ( X H Y ) C_ ( X J Y ) )
Theorem	sscres 15727	Any function restricted to a square domain is a subcategory subset of the original. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ( H Fn ( S X. S ) /\ S e. V ) -> ( H |` ( T X. T ) ) C_cat H )
Theorem	sscid 15728	The subcategory subset relation is reflexive. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ( H Fn ( S X. S ) /\ S e. V ) -> H C_cat H )
Theorem	ssctr 15729	The subcategory subset relation is transitive. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ( A C_cat B /\ B C_cat C ) -> A C_cat C )
Theorem	ssceq 15730	The subcategory subset relation is antisymmetric. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ( A C_cat B /\ B C_cat A ) -> A = B )
Theorem	rescval 15731	Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat H )   =>    |- ( ( C e. V /\ H e. W ) -> D = ( ( C ↾s dom dom H ) sSet <. ( Hom ` ndx ) , H >. ) )
Theorem	rescval2 15732	Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat H )   &    |- ( ph -> C e. V )   &    |- ( ph -> S e. W )   &    |- ( ph -> H Fn ( S X. S ) )   =>    |- ( ph -> D = ( ( C ↾s S ) sSet <. ( Hom ` ndx ) , H >. ) )
Theorem	rescbas 15733	Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat H )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. V )   &    |- ( ph -> H Fn ( S X. S ) )   &    |- ( ph -> S C_ B )   =>    |- ( ph -> S = ( Base ` D ) )
Theorem	reschom 15734	Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat H )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. V )   &    |- ( ph -> H Fn ( S X. S ) )   &    |- ( ph -> S C_ B )   =>    |- ( ph -> H = ( Hom ` D ) )
Theorem	reschomf 15735	Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat H )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. V )   &    |- ( ph -> H Fn ( S X. S ) )   &    |- ( ph -> S C_ B )   =>    |- ( ph -> H = ( Hom f ` D ) )
Theorem	rescco 15736	Composition in the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat H )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. V )   &    |- ( ph -> H Fn ( S X. S ) )   &    |- ( ph -> S C_ B )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = (comp ` D ) )
Theorem	rescabs 15737	Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> C e. V )   &    |- ( ph -> H Fn ( S X. S ) )   &    |- ( ph -> J Fn ( T X. T ) )   &    |- ( ph -> S e. W )   &    |- ( ph -> T C_ S )   =>    |- ( ph -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) )
Theorem	rescabs2 15738	Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> C e. V )   &    |- ( ph -> J Fn ( T X. T ) )   &    |- ( ph -> S e. W )   &    |- ( ph -> T C_ S )   =>    |- ( ph -> ( ( C ↾s S ) |`cat J ) = ( C |`cat J ) )
Theorem	issubc 15739*	Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- H = ( Hom f ` C )   &    |- .1. = ( Id ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> S = dom dom J )   =>    |- ( ph -> ( J e. (Subcat ` C ) <-> ( J C_cat H /\ A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) ) ) ) )
Theorem	issubc2 15740*	Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- H = ( Hom f ` C )   &    |- .1. = ( Id ` C )   &    |- .x. = (comp ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> J Fn ( S X. S ) )   =>    |- ( ph -> ( J e. (Subcat ` C ) <-> ( J C_cat H /\ A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) ) ) ) )
Theorem	0ssc 15741	For any category C, the empty set is a subcategory subset of C. (Contributed by AV, 23-Apr-2020.)
|- ( C e. Cat -> (/) C_cat ( Hom f ` C ) )
Theorem	0subcat 15742	For any category C, the empty set is a (full) subcategory of C, see example 4.3(1.a) in [Adamek] p. 48. (Contributed by AV, 23-Apr-2020.)
|- ( C e. Cat -> (/) e. (Subcat ` C ) )
Theorem	catsubcat 15743	For any category C, C itself is a (full) subcategory of C, see example 4.3(1.b) in [Adamek] p. 48. (Contributed by AV, 23-Apr-2020.)
|- ( C e. Cat -> ( Hom f ` C ) e. (Subcat ` C ) )
Theorem	subcssc 15744	An element in the set of subcategories is a subset of the category. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> J e. (Subcat ` C ) )   &    |- H = ( Hom f ` C )   =>    |- ( ph -> J C_cat H )
Theorem	subcfn 15745	An element in the set of subcategories is a binary function. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> J e. (Subcat ` C ) )   &    |- ( ph -> S = dom dom J )   =>    |- ( ph -> J Fn ( S X. S ) )
Theorem	subcss1 15746	The objects of a subcategory are a subset of the objects of the original. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> J e. (Subcat ` C ) )   &    |- ( ph -> J Fn ( S X. S ) )   &    |- B = ( Base ` C )   =>    |- ( ph -> S C_ B )
Theorem	subcss2 15747	The morphisms of a subcategory are a subset of the morphisms of the original. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> J e. (Subcat ` C ) )   &    |- ( ph -> J Fn ( S X. S ) )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   =>    |- ( ph -> ( X J Y ) C_ ( X H Y ) )
Theorem	subcidcl 15748	The identity of the original category is contained in each subcategory. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> J e. (Subcat ` C ) )   &    |- ( ph -> J Fn ( S X. S ) )   &    |- ( ph -> X e. S )   &    |- .1. = ( Id ` C )   =>    |- ( ph -> ( .1. ` X ) e. ( X J X ) )
Theorem	subccocl 15749	A subcategory is closed under composition. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( ph -> J e. (Subcat ` C ) )   &    |- ( ph -> J Fn ( S X. S ) )   &    |- ( ph -> X e. S )   &    |- .x. = (comp ` C )   &    |- ( ph -> Y e. S )   &    |- ( ph -> Z e. S )   &    |- ( ph -> F e. ( X J Y ) )   &    |- ( ph -> G e. ( Y J Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) )
Theorem	subccatid 15750*	A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat J )   &    |- ( ph -> J e. (Subcat ` C ) )   &    |- ( ph -> J Fn ( S X. S ) )   &    |- .1. = ( Id ` C )   =>    |- ( ph -> ( D e. Cat /\ ( Id ` D ) = ( x e. S |-> ( .1. ` x ) ) ) )
Theorem	subcid 15751	The identity in a subcategory is the same as the original category. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat J )   &    |- ( ph -> J e. (Subcat ` C ) )   &    |- ( ph -> J Fn ( S X. S ) )   &    |- .1. = ( Id ` C )   &    |- ( ph -> X e. S )   =>    |- ( ph -> ( .1. ` X ) = ( ( Id ` D ) ` X ) )
Theorem	subccat 15752	A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- D = ( C |`cat J )   &    |- ( ph -> J e. (Subcat ` C ) )   =>    |- ( ph -> D e. Cat )
Theorem	issubc3 15753*	Alternate definition of a subcategory, as a subset of the category which is itself a category. The assumption that the identity be closed is necessary just as in the case of a monoid, issubm2 16594, for the same reasons, since categories are a generalization of monoids. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- H = ( Hom f ` C )   &    |- .1. = ( Id ` C )   &    |- D = ( C |`cat J )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> J Fn ( S X. S ) )   =>    |- ( ph -> ( J e. (Subcat ` C ) <-> ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) )
Theorem	fullsubc 15754	The full subcategory generated by a subset of objects is the category with these objects and the same morphisms as the original. The result is always a subcategory (and it is full, meaning that all morphisms of the original category between objects in the subcategory is also in the subcategory), see definition 4.1(2) of [Adamek] p. 48. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom f ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> S C_ B )   =>    |- ( ph -> ( H |` ( S X. S ) ) e. (Subcat ` C ) )
Theorem	fullresc 15755	The category formed by structure restriction is the same as the category restriction. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom f ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> S C_ B )   &    |- D = ( C ↾s S )   &    |- E = ( C |`cat ( H |` ( S X. S ) ) )   =>    |- ( ph -> ( ( Hom f ` D ) = ( Hom f ` E ) /\ (compf ` D ) = (compf ` E ) ) )
Theorem	resscat 15756	A category restricted to a smaller set of objects is a category. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ( C e. Cat /\ S e. V ) -> ( C ↾s S ) e. Cat )
Theorem	subsubc 15757	A subcategory of a subcategory is a subcategory. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- D = ( C |`cat H )   =>    |- ( H e. (Subcat ` C ) -> ( J e. (Subcat ` D ) <-> ( J e. (Subcat ` C ) /\ J C_cat H ) ) )
8.1.7  Functors
Syntax	cfunc 15758	Extend class notation with the class of all functors.
class Func
Syntax	cidfu 15759	Extend class notation with identity functor.
class idfunc
Syntax	ccofu 15760	Extend class notation with functor composition.
class o.func
Syntax	cresf 15761	Extend class notation to include restriction of a functor to a subcategory.
class |`f
Definition	df-func 15762*	Function returning all the functors from a category t to a category u. Definition 3.17 of [Adamek] p. 29, and definition in [Lang] p. 62 ("covariant functor"). Intuitively a functor associates any morphism of t to a morphism of u, any object of t to an object of u, and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of t to an object of u we write it associates any identity of t to an identity of u which simplifies the definition. According to remark 3.19 in [Adamek] p. 30, "a functor F : A -> B is technically a family of functions; one from Ob(A) to Ob(B) [here: f, called "the object part" in the following], and for each pair (A,A') of A-objects, one from hom(A,A') to hom(FA, FA') [here: g, called "the morphism part" in the following]". (Contributed by FL, 10-Feb-2008.) (Revised by Mario Carneiro, 2-Jan-2017.)
|- Func = ( t e. Cat , u e. Cat |-> { <. f , g >. | [. ( Base ` t ) / b ]. ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. (comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) } )
Definition	df-idfu 15763*	Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- idfunc = ( t e. Cat |-> [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. )
Definition	df-cofu 15764*	Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )
Definition	df-resf 15765*	Define the restriction of a functor to a subcategory (analogue of df-res 4865). (Contributed by Mario Carneiro, 6-Jan-2017.)
|- |`f = ( f e. _V , h e. _V |-> <. ( ( 1st ` f ) |` dom dom h ) , ( x e. dom h |-> ( ( ( 2nd ` f ) ` x ) |` ( h ` x ) ) ) >. )
Theorem	relfunc 15766	The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- Rel ( D Func E )
Theorem	funcrcl 15767	Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( F e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )
Theorem	isfunc 15768*	Value of the set of functors between two categories. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- C = ( Base ` E )   &    |- H = ( Hom ` D )   &    |- J = ( Hom ` E )   &    |- .1. = ( Id ` D )   &    |- I = ( Id ` E )   &    |- .x. = (comp ` D )   &    |- O = (comp ` E )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   =>    |- ( ph -> ( F ( D Func E ) G <-> ( F : B --> C /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. B ( ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) ) )
Theorem	isfuncd 15769*	Deduce that an operation is a functor of categories. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- B = ( Base ` D )   &    |- C = ( Base ` E )   &    |- H = ( Hom ` D )   &    |- J = ( Hom ` E )   &    |- .1. = ( Id ` D )   &    |- I = ( Id ` E )   &    |- .x. = (comp ` D )   &    |- O = (comp ` E )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> F : B --> C )   &    |- ( ph -> G Fn ( B X. B ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )   &    |- ( ( ph /\ x e. B ) -> ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) )   =>    |- ( ph -> F ( D Func E ) G )
Theorem	funcf1 15770	The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- C = ( Base ` E )   &    |- ( ph -> F ( D Func E ) G )   =>    |- ( ph -> F : B --> C )
Theorem	funcixp 15771*	The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- H = ( Hom ` D )   &    |- J = ( Hom ` E )   &    |- ( ph -> F ( D Func E ) G )   =>    |- ( ph -> G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
Theorem	funcf2 15772	The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- H = ( Hom ` D )   &    |- J = ( Hom ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X G Y ) : ( X H Y ) --> ( ( F ` X ) J ( F ` Y ) ) )
Theorem	funcfn2 15773	The morphism part of a functor is a function. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` D )   &    |- ( ph -> F ( D Func E ) G )   =>    |- ( ph -> G Fn ( B X. B ) )
Theorem	funcid 15774	A functor maps each identity to the corresponding identity in the target category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- .1. = ( Id ` D )   &    |- I = ( Id ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( X G X ) ` ( .1. ` X ) ) = ( I ` ( F ` X ) ) )
Theorem	funcco 15775	A functor maps composition in the source category to composition in the target. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- H = ( Hom ` D )   &    |- .x. = (comp ` D )   &    |- O = (comp ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> M e. ( X H Y ) )   &    |- ( ph -> N e. ( Y H Z ) )   =>    |- ( ph -> ( ( X G Z ) ` ( N ( <. X , Y >. .x. Z ) M ) ) = ( ( ( Y G Z ) ` N ) ( <. ( F ` X ) , ( F ` Y ) >. O ( F ` Z ) ) ( ( X G Y ) ` M ) ) )
Theorem	funcsect 15776	The image of a section under a functor is a section. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` D )   &    |- S = (Sect ` D )   &    |- T = (Sect ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> M ( X S Y ) N )   =>    |- ( ph -> ( ( X G Y ) ` M ) ( ( F ` X ) T ( F ` Y ) ) ( ( Y G X ) ` N ) )
Theorem	funcinv 15777	The image of an inverse under a functor is an inverse. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` D )   &    |- I = (Inv ` D )   &    |- J = (Inv ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> M ( X I Y ) N )   =>    |- ( ph -> ( ( X G Y ) ` M ) ( ( F ` X ) J ( F ` Y ) ) ( ( Y G X ) ` N ) )
Theorem	funciso 15778	The image of an isomorphism under a functor is an isomorphism. Proposition 3.21 of [Adamek] p. 32. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` D )   &    |- I = ( Iso ` D )   &    |- J = ( Iso ` E )   &    |- ( ph -> F ( D Func E ) G )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> M e. ( X I Y ) )   =>    |- ( ph -> ( ( X G Y ) ` M ) e. ( ( F ` X ) J ( F ` Y ) ) )
Theorem	funcoppc 15779	A functor on categories yields a functor on the opposite categories (in the same direction), see definition 3.41 of [Adamek] p. 39. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- O = (oppCat ` C )   &    |- P = (oppCat ` D )   &    |- ( ph -> F ( C Func D ) G )   =>    |- ( ph -> F ( O Func P )tpos G )
Theorem	idfuval 15780*	Value of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- H = ( Hom ` C )   =>    |- ( ph -> I = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
Theorem	idfu2nd 15781	Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( 2nd ` I ) Y ) = ( _I |` ( X H Y ) ) )
Theorem	idfu2 15782	Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- I = (idfunc ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( ( X ( 2nd ` I ) Y ) ` F ) = F )
Theorem	idfu1st 15783	Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   =>    |- ( ph -> ( 1st ` I ) = ( _I |` B ) )
Theorem	idfu1 15784	Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( 1st ` I ) ` X ) = X )
Theorem	idfucl 15785	The identity functor is a functor. Example 3.20(1) of [Adamek] p. 30. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   =>    |- ( C e. Cat -> I e. ( C Func C ) )
Theorem	cofuval 15786*	Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   =>    |- ( ph -> ( G o.func F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
Theorem	cofu1st 15787	Value of the object part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   =>    |- ( ph -> ( 1st ` ( G o.func F ) ) = ( ( 1st ` G ) o. ( 1st ` F ) ) )
Theorem	cofu1 15788	Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( 1st ` ( G o.func F ) ) ` X ) = ( ( 1st ` G ) ` ( ( 1st ` F ) ` X ) ) )
Theorem	cofu2nd 15789	Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( 2nd ` ( G o.func F ) ) Y ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) )
Theorem	cofu2 15790	Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- H = ( Hom ` C )   &    |- ( ph -> R e. ( X H Y ) )   =>    |- ( ph -> ( ( X ( 2nd ` ( G o.func F ) ) Y ) ` R ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) )
Theorem	cofuval2 15791*	Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- ( ph -> F ( C Func D ) G )   &    |- ( ph -> H ( D Func E ) K )   =>    |- ( ph -> ( <. H , K >. o.func <. F , G >. ) = <. ( H o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) K ( F ` y ) ) o. ( x G y ) ) ) >. )
Theorem	cofucl 15792	The composition of two functors is a functor. Proposition 3.23 of [Adamek] p. 33. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( D Func E ) )   =>    |- ( ph -> ( G o.func F ) e. ( C Func E ) )
Theorem	cofuass 15793	Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> G e. ( C Func D ) )   &    |- ( ph -> H e. ( D Func E ) )   &    |- ( ph -> K e. ( E Func F ) )   =>    |- ( ph -> ( ( K o.func H ) o.func G ) = ( K o.func ( H o.func G ) ) )
Theorem	cofulid 15794	The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> F e. ( C Func D ) )   &    |- I = (idfunc ` D )   =>    |- ( ph -> ( I o.func F ) = F )
Theorem	cofurid 15795	The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- ( ph -> F e. ( C Func D ) )   &    |- I = (idfunc ` C )   =>    |- ( ph -> ( F o.func I ) = F )
Theorem	resfval 15796*	Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> H e. W )   =>    |- ( ph -> ( F |`f H ) = <. ( ( 1st ` F ) |` dom dom H ) , ( x e. dom H |-> ( ( ( 2nd ` F ) ` x ) |` ( H ` x ) ) ) >. )
Theorem	resfval2 15797*	Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> H e. W )   &    |- ( ph -> G e. X )   &    |- ( ph -> H Fn ( S X. S ) )   =>    |- ( ph -> ( <. F , G >. |`f H ) = <. ( F |` S ) , ( x e. S , y e. S |-> ( ( x G y ) |` ( x H y ) ) ) >. )
Theorem	resf1st 15798	Value of the functor restriction operator on objects. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> H e. W )   &    |- ( ph -> H Fn ( S X. S ) )   =>    |- ( ph -> ( 1st ` ( F |`f H ) ) = ( ( 1st ` F ) |` S ) )
Theorem	resf2nd 15799	Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> H e. W )   &    |- ( ph -> H Fn ( S X. S ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. S )   =>    |- ( ph -> ( X ( 2nd ` ( F |`f H ) ) Y ) = ( ( X ( 2nd ` F ) Y ) |` ( X H Y ) ) )
Theorem	funcres 15800	A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> H e. (Subcat ` C ) )   =>    |- ( ph -> ( F |`f H ) e. ( ( C |`cat H ) Func D ) )