P. 160 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15901-16000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	initoo 15901	An initial object is an object. (Contributed by AV, 14-Apr-2020.)
|- ( C e. Cat -> ( O e. (InitO ` C ) -> O e. ( Base ` C ) ) )
Theorem	termoo 15902	A terminal object is an object. (Contributed by AV, 18-Apr-2020.)
|- ( C e. Cat -> ( O e. (TermO ` C ) -> O e. ( Base ` C ) ) )
Theorem	iszeroi 15903	Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020.)
|- ( ( C e. Cat /\ O e. (ZeroO ` C ) ) -> ( O e. ( Base ` C ) /\ ( O e. (InitO ` C ) /\ O e. (TermO ` C ) ) ) )
Theorem	2initoinv 15904	Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- ( ph -> A e. (InitO ` C ) )   &    |- ( ph -> B e. (InitO ` C ) )   =>    |- ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> F ( A (Inv ` C ) B ) G )
Theorem	initoeu1 15905*	Initial objects are essentially unique (strong form), i.e. there is a unique isomorphism between two initial objects, see statement in [Lang] p. 58 ("... if P, P' are two universal objects [...] then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 14-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- ( ph -> A e. (InitO ` C ) )   &    |- ( ph -> B e. (InitO ` C ) )   =>    |- ( ph -> E! f f e. ( A ( Iso ` C ) B ) )
Theorem	initoeu1w 15906	Initial objects are essentially unique (weak form), i.e. if A and B are initial objects, then A and B are isomorphic. Proposition 7.3 (1) of [Adamek] p. 102. (Contributed by AV, 6-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- ( ph -> A e. (InitO ` C ) )   &    |- ( ph -> B e. (InitO ` C ) )   =>    |- ( ph -> A ( ~=c𝑐 ` C ) B )
Theorem	initoeu2lem0 15907	Lemma 0 for initoeu2 15910. (Contributed by AV, 9-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- ( ph -> A e. (InitO ` C ) )   &    |- X = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- I = ( Iso ` C )   &    |- .o. = (comp ` C )   =>    |- ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B (Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B (Inv ` C ) A ) ` K ) ) ) -> G = ( F ( <. B , A >. .o. D ) K ) )
Theorem	initoeu2lem1 15908*	Lemma 1 for initoeu2 15910. (Contributed by AV, 9-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- ( ph -> A e. (InitO ` C ) )   &    |- X = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- I = ( Iso ` C )   &    |- .o. = (comp ` C )   =>    |- ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) -> ( ( E! f f e. ( A H D ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) -> G = ( F ( <. B , A >. .o. D ) K ) ) )
Theorem	initoeu2lem2 15909*	Lemma 2 for initoeu2 15910. (Contributed by AV, 10-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- ( ph -> A e. (InitO ` C ) )   &    |- X = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- I = ( Iso ` C )   &    |- .o. = (comp ` C )   =>    |- ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) -> ( E! f f e. ( A H D ) -> E! g g e. ( B H D ) ) )
Theorem	initoeu2 15910	Initial objects are essentially unique, if A is an initial object, then so is every object that is isomorphic to A. Proposition 7.3 (2) in [Adamek] p. 102. (Contributed by AV, 10-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- ( ph -> A e. (InitO ` C ) )   &    |- ( ph -> A ( ~=c𝑐 ` C ) B )   =>    |- ( ph -> B e. (InitO ` C ) )
Theorem	2termoinv 15911	Morphisms between two terminal objects are inverses. (Contributed by AV, 18-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- ( ph -> A e. (TermO ` C ) )   &    |- ( ph -> B e. (TermO ` C ) )   =>    |- ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> F ( A (Inv ` C ) B ) G )
Theorem	termoeu1 15912*	Terminal objects are essentially unique (strong form), i.e. there is a unique isomorphism between two terminal objects, see statement in [Lang] p. 58 ("... if P, P' are two universal objects [...] then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 18-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- ( ph -> A e. (TermO ` C ) )   &    |- ( ph -> B e. (TermO ` C ) )   =>    |- ( ph -> E! f f e. ( A ( Iso ` C ) B ) )
Theorem	termoeu1w 15913	Terminal objects are essentially unique (weak form), i.e. if A and B are terminal objects, then A and B are isomorphic. Proposition 7.6 of [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- ( ph -> A e. (TermO ` C ) )   &    |- ( ph -> B e. (TermO ` C ) )   =>    |- ( ph -> A ( ~=c𝑐 ` C ) B )
8.2  Arrows (disjointified hom-sets)
Syntax	cdoma 15914	Extend class notation to include the domain extractor for an arrow.
class domA
Syntax	ccoda 15915	Extend class notation to include the codomain extractor for an arrow.
class coda
Syntax	carw 15916	Extend class notation to include the collection of all arrows of a category.
class Nat
Syntax	choma 15917	Extend class notation to include the set of all arrows with a specific domain and codomain.
class Homa
Definition	df-doma 15918	Definition of the domain extractor for an arrow. (Contributed by FL, 24-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
|- domA = ( 1st o. 1st )
Definition	df-coda 15919	Definition of the codomain extractor for an arrow. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
|- coda = ( 2nd o. 1st )
Definition	df-homa 15920*	Definition of the hom-set extractor for arrows, which tags the morphisms of the underlying hom-set with domain and codomain, which can then be extracted using df-doma 15918 and df-coda 15919. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
|- Homa = ( c e. Cat |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )
Definition	df-arw 15921	Definition of the set of arrows of a category. We will use the term "arrow" to denote a morphism tagged with its domain and codomain, as opposed to Hom, which allows hom-sets for distinct objects to overlap. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- Nat = ( c e. Cat |-> U. ran (Homa ` c ) )
Theorem	homarcl 15922	Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   =>    |- ( F e. ( X H Y ) -> C e. Cat )
Theorem	homafval 15923*	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- J = ( Hom ` C )   =>    |- ( ph -> H = ( x e. ( B X. B ) |-> ( { x } X. ( J ` x ) ) ) )
Theorem	homaf 15924	Functionality of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   =>    |- ( ph -> H : ( B X. B ) --> ~P ( ( B X. B ) X. _V ) )
Theorem	homaval 15925	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- J = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( { <. X , Y >. } X. ( X J Y ) ) )
Theorem	elhoma 15926	Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- J = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( Z ( X H Y ) F <-> ( Z = <. X , Y >. /\ F e. ( X J Y ) ) ) )
Theorem	elhomai 15927	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- J = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X J Y ) )   =>    |- ( ph -> <. X , Y >. ( X H Y ) F )
Theorem	elhomai2 15928	Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- J = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X J Y ) )   =>    |- ( ph -> <. X , Y , F >. e. ( X H Y ) )
Theorem	homarcl2 15929	Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- B = ( Base ` C )   =>    |- ( F e. ( X H Y ) -> ( X e. B /\ Y e. B ) )
Theorem	homarel 15930	An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   =>    |- Rel ( X H Y )
Theorem	homa1 15931	The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   =>    |- ( Z ( X H Y ) F -> Z = <. X , Y >. )
Theorem	homahom2 15932	The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- J = ( Hom ` C )   =>    |- ( Z ( X H Y ) F -> F e. ( X J Y ) )
Theorem	homahom 15933	The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- J = ( Hom ` C )   =>    |- ( F e. ( X H Y ) -> ( 2nd ` F ) e. ( X J Y ) )
Theorem	homadm 15934	The domain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   =>    |- ( F e. ( X H Y ) -> (domA ` F ) = X )
Theorem	homacd 15935	The codomain of an arrow with known domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   =>    |- ( F e. ( X H Y ) -> (coda ` F ) = Y )
Theorem	homadmcd 15936	Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   =>    |- ( F e. ( X H Y ) -> F = <. X , Y , ( 2nd ` F ) >. )
Theorem	arwval 15937	The set of arrows is the union of all the disjointified hom-sets. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- A = (Nat ` C )   &    |- H = (Homa ` C )   =>    |- A = U. ran H
Theorem	arwrcl 15938	The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- A = (Nat ` C )   =>    |- ( F e. A -> C e. Cat )
Theorem	arwhoma 15939	An arrow is contained in the hom-set corresponding to its domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- A = (Nat ` C )   &    |- H = (Homa ` C )   =>    |- ( F e. A -> F e. ( (domA ` F ) H (coda ` F ) ) )
Theorem	homarw 15940	A hom-set is a subset of the collection of all arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- A = (Nat ` C )   &    |- H = (Homa ` C )   =>    |- ( X H Y ) C_ A
Theorem	arwdm 15941	The domain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- A = (Nat ` C )   &    |- B = ( Base ` C )   =>    |- ( F e. A -> (domA ` F ) e. B )
Theorem	arwcd 15942	The codomain of an arrow is an object. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- A = (Nat ` C )   &    |- B = ( Base ` C )   =>    |- ( F e. A -> (coda ` F ) e. B )
Theorem	dmaf 15943	The domain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- A = (Nat ` C )   &    |- B = ( Base ` C )   =>    |- (domA |` A ) : A --> B
Theorem	cdaf 15944	The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- A = (Nat ` C )   &    |- B = ( Base ` C )   =>    |- (coda |` A ) : A --> B
Theorem	arwhom 15945	The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017.)
|- A = (Nat ` C )   &    |- J = ( Hom ` C )   =>    |- ( F e. A -> ( 2nd ` F ) e. ( (domA ` F ) J (coda ` F ) ) )
Theorem	arwdmcd 15946	Decompose an arrow into domain, codomain, and morphism. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- A = (Nat ` C )   =>    |- ( F e. A -> F = <. (domA ` F ) , (coda ` F ) , ( 2nd ` F ) >. )
8.2.1  Identity and composition for arrows
Syntax	cida 15947	Extend class notation to include identity for arrows.
class Ida
Syntax	ccoa 15948	Extend class notation to include composition for arrows.
class compa
Definition	df-ida 15949*	Definition of the identity arrow, which is just the identity morphism tagged with its domain and codomain. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
|- Ida = ( c e. Cat |-> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) )
Definition	df-coa 15950*	Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a 5-ary operation like the regular composition in a category comp. Instead, it is a partial binary operation on arrows, which is defined when the domain of the first arrow matches the codomain of the second. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- compa = ( c e. Cat |-> ( g e. (Nat ` c ) , f e. { h e. (Nat ` c ) | (coda ` h ) = (domA ` g ) } |-> <. (domA ` f ) , (coda ` g ) , ( ( 2nd ` g ) ( <. (domA ` f ) , (domA ` g ) >. (comp ` c ) (coda ` g ) ) ( 2nd ` f ) ) >. ) )
Theorem	idafval 15951*	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- I = (Ida ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- .1. = ( Id ` C )   =>    |- ( ph -> I = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )
Theorem	idaval 15952	Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- I = (Ida ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- .1. = ( Id ` C )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( I ` X ) = <. X , X , ( .1. ` X ) >. )
Theorem	ida2 15953	Morphism part of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- I = (Ida ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- .1. = ( Id ` C )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( 2nd ` ( I ` X ) ) = ( .1. ` X ) )
Theorem	idahom 15954	Domain and codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- I = (Ida ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- H = (Homa ` C )   =>    |- ( ph -> ( I ` X ) e. ( X H X ) )
Theorem	idadm 15955	Domain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- I = (Ida ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> (domA ` ( I ` X ) ) = X )
Theorem	idacd 15956	Codomain of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- I = (Ida ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> (coda ` ( I ` X ) ) = X )
Theorem	idaf 15957	The identity arrow function is a function from objects to arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- I = (Ida ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- A = (Nat ` C )   =>    |- ( ph -> I : B --> A )
Theorem	coafval 15958*	The value of the composition of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- A = (Nat ` C )   &    |- .xb = (comp ` C )   =>    |- .x. = ( g e. A , f e. { h e. A | (coda ` h ) = (domA ` g ) } |-> <. (domA ` f ) , (coda ` g ) , ( ( 2nd ` g ) ( <. (domA ` f ) , (domA ` g ) >. .xb (coda ` g ) ) ( 2nd ` f ) ) >. )
Theorem	eldmcoa 15959	A pair <. G , F >. is in the domain of the arrow composition, if the domain of G equals the codomain of F. (In this case we say G and F are composable.) (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- A = (Nat ` C )   =>    |- ( G dom .x. F <-> ( F e. A /\ G e. A /\ (coda ` F ) = (domA ` G ) ) )
Theorem	dmcoass 15960	The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- A = (Nat ` C )   =>    |- dom .x. C_ ( A X. A )
Theorem	homdmcoa 15961	If F : X --> Y and G : Y --> Z, then G and F are composable. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- H = (Homa ` C )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   =>    |- ( ph -> G dom .x. F )
Theorem	coaval 15962	Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- H = (Homa ` C )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   &    |- .xb = (comp ` C )   =>    |- ( ph -> ( G .x. F ) = <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) >. )
Theorem	coa2 15963	The morphism part of arrow composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- H = (Homa ` C )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   &    |- .xb = (comp ` C )   =>    |- ( ph -> ( 2nd ` ( G .x. F ) ) = ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) )
Theorem	coahom 15964	The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- H = (Homa ` C )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   =>    |- ( ph -> ( G .x. F ) e. ( X H Z ) )
Theorem	coapm 15965	Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- A = (Nat ` C )   =>    |- .x. e. ( A ^pm ( A X. A ) )
Theorem	arwlid 15966	Left identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- .x. = (compa ` C )   &    |- .1. = (Ida ` C )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( ( .1. ` Y ) .x. F ) = F )
Theorem	arwrid 15967	Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- .x. = (compa ` C )   &    |- .1. = (Ida ` C )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( F .x. ( .1. ` X ) ) = F )
Theorem	arwass 15968	Associativity of composition in a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- .x. = (compa ` C )   &    |- .1. = (Ida ` C )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   &    |- ( ph -> K e. ( Z H W ) )   =>    |- ( ph -> ( ( K .x. G ) .x. F ) = ( K .x. ( G .x. F ) ) )
8.3  Examples of categories
8.3.1  The category of sets
Syntax	csetc 15969	Extend class notation to include the category Set.
class SetCat
Definition	df-setc 15970*	Definition of the category Set, relativized to a subset u. Example 3.3(1) of [Adamek] p. 22. This is the category of all sets in u and functions between these sets. Generally, we will take u to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by FL, 8-Nov-2013.) (Revised by Mario Carneiro, 3-Jan-2017.)
|- SetCat = ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( y ^m x ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. } )
Theorem	setcval 15971*	Value of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> H = ( x e. U , y e. U |-> ( y ^m x ) ) )   &    |- ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	setcbas 15972	Set of objects of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   =>    |- ( ph -> U = ( Base ` C ) )
Theorem	setchomfval 15973*	Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. U , y e. U |-> ( y ^m x ) ) )
Theorem	setchom 15974	Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( X H Y ) = ( Y ^m X ) )
Theorem	elsetchom 15975	A morphism of sets is a function. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( F e. ( X H Y ) <-> F : X --> Y ) )
Theorem	setccofval 15976*	Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) )
Theorem	setcco 15977	Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- ( ph -> Z e. U )   &    |- ( ph -> F : X --> Y )   &    |- ( ph -> G : Y --> Z )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )
Theorem	setccatid 15978*	Lemma for setccat 15979. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` x ) ) ) )
Theorem	setccat 15979	The category of sets is a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	setcid 15980	The identity arrow in the category of sets is the identity function. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` X ) )
Theorem	setcmon 15981	A monomorphism of sets is an injection. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- M = (Mono ` C )   =>    |- ( ph -> ( F e. ( X M Y ) <-> F : X -1-1-> Y ) )
Theorem	setcepi 15982	An epimorphism of sets is a surjection. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- E = (Epi ` C )   &    |- ( ph -> 2o e. U )   =>    |- ( ph -> ( F e. ( X E Y ) <-> F : X -onto-> Y ) )
Theorem	setcsect 15983	A section in the category of sets, written out. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- S = (Sect ` C )   =>    |- ( ph -> ( F ( X S Y ) G <-> ( F : X --> Y /\ G : Y --> X /\ ( G o. F ) = ( _I |` X ) ) ) )
Theorem	setcinv 15984	An inverse in the category of sets is the converse operation. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- N = (Inv ` C )   =>    |- ( ph -> ( F ( X N Y ) G <-> ( F : X -1-1-onto-> Y /\ G = `' F ) ) )
Theorem	setciso 15985	An isomorphism in the category of sets is a bijection. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( F e. ( X I Y ) <-> F : X -1-1-onto-> Y ) )
Theorem	resssetc 15986	The restriction of the category of sets to a subset is the category of sets in the subset. Thus, the SetCat ` U categories for different U are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- C = ( SetCat ` U )   &    |- D = ( SetCat ` V )   &    |- ( ph -> U e. W )   &    |- ( ph -> V C_ U )   =>    |- ( ph -> ( ( Hom f ` ( C ↾s V ) ) = ( Hom f ` D ) /\ (compf ` ( C ↾s V ) ) = (compf ` D ) ) )
Theorem	funcsetcres2 15987	A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- C = ( SetCat ` U )   &    |- D = ( SetCat ` V )   &    |- ( ph -> U e. W )   &    |- ( ph -> V C_ U )   =>    |- ( ph -> ( E Func D ) C_ ( E Func C ) )
8.3.2  The category of categories
Syntax	ccatc 15988	Extend class notation to include the category Cat.
class CatCat
Definition	df-catc 15989*	Definition of the category Cat, which consists of all categories in the universe u (i.e. "small categories", see definition 3.44. of [Adamek] p. 39), with functors as the morphisms. Definition 3.47 of [Adamek] p. 40. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- CatCat = ( u e. _V |-> [_ ( u i^i Cat ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } )
Theorem	catcval 15990*	Value of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Cat ) )   &    |- ( ph -> H = ( x e. B , y e. B |-> ( x Func y ) ) )   &    |- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	catcbas 15991	Set of objects of the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Cat ) )
Theorem	catchomfval 15992*	Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. B , y e. B |-> ( x Func y ) ) )
Theorem	catchom 15993	Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X Func Y ) )
Theorem	catccofval 15994*	Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) )
Theorem	catcco 15995	Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X Func Y ) )   &    |- ( ph -> G e. ( Y Func Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o.func F ) )
Theorem	catccatid 15996*	Lemma for catccat 15998. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> (idfunc ` x ) ) ) )
Theorem	catcid 15997	The identity arrow in the category of categories is the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- I = (idfunc ` X )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( .1. ` X ) = I )
Theorem	catccat 15998	The category of categories is a category, see remark 3.48 in [Adamek] p. 40. (Clearly it cannot be an element of itself, hence it is "large" with respect to U.) (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	resscatc 15999	The restriction of the category of categories to a subset is the category of categories in the subset. Thus, the CatCat ` U categories for different U are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- C = (CatCat ` U )   &    |- D = (CatCat ` V )   &    |- ( ph -> U e. W )   &    |- ( ph -> V C_ U )   =>    |- ( ph -> ( ( Hom f ` ( C ↾s V ) ) = ( Hom f ` D ) /\ (compf ` ( C ↾s V ) ) = (compf ` D ) ) )
Theorem	catcisolem 16000*	Lemma for catciso 16001. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- R = ( Base ` X )   &    |- S = ( Base ` Y )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = (Inv ` C )   &    |- H = ( x e. S , y e. S |-> `' ( ( `' F ` x ) G ( `' F ` y ) ) )   &    |- ( ph -> F ( ( X Full Y ) i^i ( X Faith Y ) ) G )   &    |- ( ph -> F : R -1-1-onto-> S )   =>    |- ( ph -> <. F , G >. ( X I Y ) <. `' F , H >. )