P. 151 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	issect2 15001	Property of being a section. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- .1. = ( Id ` C )   &    |- S = (Sect ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H X ) )   =>    |- ( ph -> ( F ( X S Y ) G <-> ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) )
Theorem	sectcan 15002	If G is a section of F and F is a section of H, then G = H. Proposition 3.10 of [Adamek] p. 28. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- S = (Sect ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> G ( X S Y ) F )   &    |- ( ph -> F ( Y S X ) H )   =>    |- ( ph -> G = H )
Theorem	sectco 15003	Composition of two sections. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- .x. = (comp ` C )   &    |- S = (Sect ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F ( X S Y ) G )   &    |- ( ph -> H ( Y S Z ) K )   =>    |- ( ph -> ( H ( <. X , Y >. .x. Z ) F ) ( X S Z ) ( G ( <. Z , Y >. .x. X ) K ) )
Theorem	invffval 15004*	Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- S = (Sect ` C )   =>    |- ( ph -> N = ( x e. B , y e. B |-> ( ( x S y ) i^i `' ( y S x ) ) ) )
Theorem	invfval 15005	Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- S = (Sect ` C )   =>    |- ( ph -> ( X N Y ) = ( ( X S Y ) i^i `' ( Y S X ) ) )
Theorem	isinv 15006	Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- S = (Sect ` C )   =>    |- ( ph -> ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ G ( Y S X ) F ) ) )
Theorem	invss 15007	The inverse relation is a relation between morphisms F : X --> Y and their inverses G : Y --> X. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- H = ( Hom ` C )   =>    |- ( ph -> ( X N Y ) C_ ( ( X H Y ) X. ( Y H X ) ) )
Theorem	invsym 15008	The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( F ( X N Y ) G <-> G ( Y N X ) F ) )
Theorem	invsym2 15009	The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> `' ( X N Y ) = ( Y N X ) )
Theorem	invfun 15010	The inverse relation is a function, which is to say that every morphism has at most one inverse. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> Fun ( X N Y ) )
Theorem	isoval 15011	The inverse relation is a function, which is to say that every morphism has at most one inverse. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( X I Y ) = dom ( X N Y ) )
Theorem	inviso1 15012	If G is an inverse to F, then F is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   &    |- ( ph -> F ( X N Y ) G )   =>    |- ( ph -> F e. ( X I Y ) )
Theorem	inviso2 15013	If G is an inverse to F, then G is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   &    |- ( ph -> F ( X N Y ) G )   =>    |- ( ph -> G e. ( Y I X ) )
Theorem	invf 15014	The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( X N Y ) : ( X I Y ) --> ( Y I X ) )
Theorem	invf1o 15015	The inverse relation is a bijection from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( X N Y ) : ( X I Y ) -1-1-onto-> ( Y I X ) )
Theorem	invinv 15016	The inverse of the inverse of an isomorphism is itself. Proposition 3.14(1) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   &    |- ( ph -> F e. ( X I Y ) )   =>    |- ( ph -> ( ( Y N X ) ` ( ( X N Y ) ` F ) ) = F )
Theorem	invco 15017	The composition of two isomorphisms is an isomorphism, and the inverse is the composition of the individual inverses. Proposition 3.14(2) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   &    |- ( ph -> F e. ( X I Y ) )   &    |- .x. = (comp ` C )   &    |- ( ph -> Z e. B )   &    |- ( ph -> G e. ( Y I Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) ( X N Z ) ( ( ( X N Y ) ` F ) ( <. Z , Y >. .x. X ) ( ( Y N Z ) ` G ) ) )
Theorem	isohom 15018	An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- I = ( Iso ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X I Y ) C_ ( X H Y ) )
Theorem	isoco 15019	The composition of two isomorphisms is an isomorphism. Proposition 3.14(2) of [Adamek] p. 29. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- .x. = (comp ` C )   &    |- I = ( Iso ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X I Y ) )   &    |- ( ph -> G e. ( Y I Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X I Z ) )
Theorem	oppcsect 15020	A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- O = (oppCat ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- S = (Sect ` C )   &    |- T = (Sect ` O )   =>    |- ( ph -> ( F ( X T Y ) G <-> G ( X S Y ) F ) )
Theorem	oppcsect2 15021	A section in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- O = (oppCat ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- S = (Sect ` C )   &    |- T = (Sect ` O )   =>    |- ( ph -> ( X T Y ) = `' ( X S Y ) )
Theorem	oppcinv 15022	An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- O = (oppCat ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = (Inv ` C )   &    |- J = (Inv ` O )   =>    |- ( ph -> ( X J Y ) = ( Y I X ) )
Theorem	oppciso 15023	An isomorphism in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- O = (oppCat ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   &    |- J = ( Iso ` O )   =>    |- ( ph -> ( X J Y ) = ( Y I X ) )
Theorem	sectmon 15024	If F is a section of G, then F is a monomorphism. A monomorphism that arises from a section is also known as a split monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- M = (Mono ` C )   &    |- S = (Sect ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F ( X S Y ) G )   =>    |- ( ph -> F e. ( X M Y ) )
Theorem	monsect 15025	If F is a monomorphism and G is a section of F, then G is an inverse of F and they are both isomorphisms. This is also stated as "a monomorphism which is also a split epimorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- M = (Mono ` C )   &    |- S = (Sect ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- N = (Inv ` C )   &    |- ( ph -> F e. ( X M Y ) )   &    |- ( ph -> G ( Y S X ) F )   =>    |- ( ph -> F ( X N Y ) G )
Theorem	sectepi 15026	If F is a section of G, then G is an epimorphism. An epimorphism that arises from a section is also known as a split epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- E = (Epi ` C )   &    |- S = (Sect ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F ( X S Y ) G )   =>    |- ( ph -> G e. ( Y E X ) )
Theorem	episect 15027	If F is an epimorphism and F is a section of G, then G is an inverse of F and they are both isomorphisms. This is also stated as "an epimorphism which is also a split monomorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- E = (Epi ` C )   &    |- S = (Sect ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- N = (Inv ` C )   &    |- ( ph -> F e. ( X E Y ) )   &    |- ( ph -> F ( X S Y ) G )   =>    |- ( ph -> F ( X N Y ) G )
8.1.5  Subcategories
Syntax	cssc 15028	Extend class notation to include the subset relation for subcategories.
class C_cat
Syntax	cresc 15029	Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms).
class |`cat
Syntax	csubc 15030	Extend class notation to include the collection of subcategories of a category.
class Subcat
Definition	df-ssc 15031*	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 15033, 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 15032*	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 15033*	(Subcat ` C ) is the set of all the subcategory specifications of the category C. Like df-subg 15988, this is not actually a collection of categories, but only sets which when given operations from the base category (using df-resc 15032) 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 15034	The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Rel C_cat
Theorem	brssc 15035*	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 15036*	An analogue of pwex 4625 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 15037	Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( H e. (Subcat ` C ) -> C e. Cat )
Theorem	sscfn1 15038	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 15039	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 15040	Lemma for ssc1 15042 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 15041*	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 15042	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 15043	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 15044	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 15045	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 15046	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 15047	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 15048	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 15049	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 15050	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 15051	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 15052	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 15053	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 15054	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 15055	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 15056*	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 15057*	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	subcssc 15058	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 15059	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 15060	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 15061	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 15062	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 15063	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 15064*	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 15065	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 15066	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 15067*	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 15784, 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 15068	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). (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 15069	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 15070	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 15071	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.6  Functors
Syntax	cfunc 15072	Extend class notation with the class of all functors.
class Func
Syntax	cidfu 15073	Extend class notation with identity functor.
class idfunc
Syntax	ccofu 15074	Extend class notation with functor composition.
class o.func
Syntax	cresf 15075	Extend class notation to include restriction of a functor to a subcategory.
class |`f
Definition	df-func 15076*	Function returning all the functors from a category t to a category u. 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. (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 15077*	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 15078*	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 15079*	Define the restriction of a functor to a subcategory (analogue of df-res 5006). (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 15080	The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- Rel ( D Func E )
Theorem	funcrcl 15081	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 15082*	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 15083*	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 15084	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 15085*	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 15086	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 15087	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 15088	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 15089	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 15090	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 15091	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 15092	The image of an isomorphism under a functor is an isomorphism. (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 15093	A functor on categories yields a functor on the opposite categories (in the same direction). (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 15094*	Value of the composition of two functors. (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 15095	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 15096	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 15097	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 15098	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 15099	The identity functor is a functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- I = (idfunc ` C )   =>    |- ( C e. Cat -> I e. ( C Func C ) )
Theorem	cofuval 15100*	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 ) ) ) >. )