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	isepi2 15701*	Write out the epimorphism property directly. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- E = (Epi ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( F e. ( X E Y ) <-> ( F e. ( X H Y ) /\ A. z e. B A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. .x. z ) F ) = ( h ( <. X , Y >. .x. z ) F ) -> g = h ) ) ) )
Theorem	epihom 15702	An epimorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- E = (Epi ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X E Y ) C_ ( X H Y ) )
Theorem	epii 15703	Property of an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   &    |- E = (Epi ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X E Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   &    |- ( ph -> K e. ( Y H Z ) )   =>    |- ( ph -> ( ( G ( <. X , Y >. .x. Z ) F ) = ( K ( <. X , Y >. .x. Z ) F ) <-> G = K ) )
8.1.4  Sections, inverses, isomorphisms
Syntax	csect 15704	Extend class notation with the sections of a morphism.
class Sect
Syntax	cinv 15705	Extend class notation with the inverses of a morphism.
class Inv
Syntax	ciso 15706	Extend class notation with the class of all isomorphisms.
class Iso
Definition	df-sect 15707*	Function returning the section relation in a category. Given arrows f : X --> Y and g : Y --> X, we say fSect g, that is, f is a section of g, if g o. f = 1 ` X. If there there is an arrow g with fSect g, the arrow f is called a section, see definition 7.19 of [Adamek] p. 106. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- Sect = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. (comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) )
Definition	df-inv 15708*	The inverse relation in a category. Given arrows f : X --> Y and g : Y --> X, we say gInv f, that is, g is an inverse of f, if g is a section of f and f is a section of g. Definition 3.8 of [Adamek] p. 28. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 2-Jan-2017.)
|- Inv = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x (Sect ` c ) y ) i^i `' ( y (Sect ` c ) x ) ) ) )
Definition	df-iso 15709*	Function returning the isomorphisms of the category c. Definition 3.8 of [Adamek] p. 28, and definition in [Lang] p. 54. (Contributed by FL, 9-Jun-2014.) (Revised by Mario Carneiro, 2-Jan-2017.)
|- Iso = ( c e. Cat |-> ( ( x e. _V |-> dom x ) o. (Inv ` c ) ) )
Theorem	sectffval 15710*	Value of the section operation. (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 -> S = ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x H y ) /\ g e. ( y H x ) ) /\ ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) } ) )
Theorem	sectfval 15711*	Value of the section relation. (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 -> ( X S Y ) = { <. f , g >. | ( ( f e. ( X H Y ) /\ g e. ( Y H X ) ) /\ ( g ( <. X , Y >. .x. X ) f ) = ( .1. ` X ) ) } )
Theorem	sectss 15712	The section relation is a relation between morphisms from X to Y and morphisms from Y to X. (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 -> ( X S Y ) C_ ( ( X H Y ) X. ( Y H X ) ) )
Theorem	issect 15713	The property " F is a section of G". (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 ( X S Y ) G <-> ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) ) )
Theorem	issect2 15714	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 15715	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 15716	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	isofval 15717*	Function value of the function returning the isomorphisms of a category. (Contributed by AV, 5-Apr-2017.)
|- ( C e. Cat -> ( Iso ` C ) = ( ( x e. _V |-> dom x ) o. (Inv ` C ) ) )
Theorem	invffval 15718*	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 15719	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 15720	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 15721	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 15722	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 15723	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 15724	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 15725	The isomorphisms are the domain of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 21-May-2020.)
|- 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 15726	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 15727	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 15728	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 15729	The inverse relation is a bijection from isomorphisms to isomorphisms. This means that every isomorphism F e. ( X I Y ) has a unique inverse, denoted by ( (Inv ` C ) ` F ). Remark 3.12 of [Adamek] p. 28. (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 15730	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 15731	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	dfiso2 15732*	Alternate definition of an isomorphism of a category, according to definition 3.8 in [Adamek] p. 28. (Contributed by AV, 10-Apr-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   &    |- I = ( Iso ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X H Y ) )   &    |- .1. = ( Id ` C )   &    |- .o. = ( <. X , Y >. (comp ` C ) X )   &    |- .* = ( <. Y , X >. (comp ` C ) Y )   =>    |- ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g .o. F ) = ( .1. ` X ) /\ ( F .* g ) = ( .1. ` Y ) ) ) )
Theorem	dfiso3 15733*	Alternate definition of an isomorphism of a category as a section in both directions. (Contributed by AV, 11-Apr-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- I = ( Iso ` C )   &    |- S = (Sect ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( g ( Y S X ) F /\ F ( X S Y ) g ) ) )
Theorem	inveq 15734	If there are two inverses of an morphism, these inverses are equal. Corollary 3.11 of [Adamek] p. 28. (Contributed by AV, 10-Apr-2017.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( F ( X N Y ) G /\ F ( X N Y ) K ) -> G = K ) )
Theorem	isofn 15735	The function value of the function returning the isomorphisms of a category is a function over the square product of the base set of the category. (Contributed by AV, 5-Apr-2017.)
|- ( C e. Cat -> ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
Theorem	isohom 15736	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 15737	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 15738	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 15739	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 15740	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 15741	An isomorphism in the opposite category. See also remark 3.9 in [Adamek] p. 28. (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 15742	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 15743	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 15744	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 15745	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 )
Theorem	sectid 15746	The identity is a section of itself. (Contributed by AV, 8-Apr-2017.)
|- B = ( Base ` C )   &    |- I = ( Id ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( I ` X ) ( X (Sect ` C ) X ) ( I ` X ) )
Theorem	invid 15747	The inverse of the identity is the identity. (Contributed by AV, 8-Apr-2017.)
|- B = ( Base ` C )   &    |- I = ( Id ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( I ` X ) ( X (Inv ` C ) X ) ( I ` X ) )
Theorem	idiso 15748	The identity is an isomorphism. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 8-Apr-2017.)
|- B = ( Base ` C )   &    |- I = ( Id ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( I ` X ) e. ( X ( Iso ` C ) X ) )
Theorem	idinv 15749	The inverse of the identity is the identity. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 9-Apr-2017.)
|- B = ( Base ` C )   &    |- I = ( Id ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( X (Inv ` C ) X ) ` ( I ` X ) ) = ( I ` X ) )
Theorem	invisoinvl 15750	The inverse of an isomorphism F (which is unique because of invf 15728 and is therefore denoted by ( ( X N Y ) ` F ), see also remark 3.12 in [Adamek] p. 28) is invers to the isomorphism. (Contributed by AV, 9-Apr-2017.)
|- B = ( Base ` C )   &    |- I = ( Iso ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X I Y ) )   =>    |- ( ph -> ( ( X N Y ) ` F ) ( Y N X ) F )
Theorem	invisoinvr 15751	The inverse of an isomorphism is invers to the isomorphism. (Contributed by AV, 9-Apr-2017.)
|- B = ( Base ` C )   &    |- I = ( Iso ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X I Y ) )   =>    |- ( ph -> F ( X N Y ) ( ( X N Y ) ` F ) )
Theorem	invcoisoid 15752	The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 5-Apr-2017.)
|- B = ( Base ` C )   &    |- I = ( Iso ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X I Y ) )   &    |- .1. = ( Id ` C )   &    |- .o. = ( <. X , Y >. (comp ` C ) X )   =>    |- ( ph -> ( ( ( X N Y ) ` F ) .o. F ) = ( .1. ` X ) )
Theorem	isocoinvid 15753	The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 10-Apr-2017.)
|- B = ( Base ` C )   &    |- I = ( Iso ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> F e. ( X I Y ) )   &    |- .1. = ( Id ` C )   &    |- .o. = ( <. Y , X >. (comp ` C ) Y )   =>    |- ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) )
Theorem	rcaninv 15754	Right cancellation of an inverse of an isomorphism. (Contributed by AV, 5-Apr-2017.)
|- B = ( Base ` C )   &    |- N = (Inv ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( Y ( Iso ` C ) X ) )   &    |- ( ph -> G e. ( Y ( Hom ` C ) Z ) )   &    |- ( ph -> H e. ( Y ( Hom ` C ) Z ) )   &    |- R = ( ( Y N X ) ` F )   &    |- .o. = ( <. X , Y >. (comp ` C ) Z )   =>    |- ( ph -> ( ( G .o. R ) = ( H .o. R ) -> G = H ) )
8.1.5  Isomorphic objects In this subsection, the "is isomorphic to" relation between objects of a category ~=c𝑐 is defined (see df-cic 15756). It is shown that this relation is an equivalence relation, see cicer 15766.
Syntax	ccic 15755	Extend class notation to include the category isomorphism relation.
class ~=c𝑐
Definition	df-cic 15756	Function returning the set of isomorphic objects for each category c. Definition 3.15 of [Adamek] p. 29. Analogous to the definition of the group isomorphism relation ~=g𝑔, see df-gic 16979. (Contributed by AV, 4-Apr-2020.)
|- ~=c𝑐 = ( c e. Cat |-> ( ( Iso ` c ) supp (/) ) )
Theorem	cicfval 15757	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 15758	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 15759*	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 15760	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 15761	Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020.)
|- ( ( C e. Cat /\ O e. ( Base ` C ) ) -> O ( ~=c𝑐 ` C ) O )
Theorem	ciclcl 15762	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 15763	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 15764	Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020.)
|- ( ( C e. Cat /\ R ( ~=c𝑐 ` C ) S ) -> S ( ~=c𝑐 ` C ) R )
Theorem	cictr 15765	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 15766	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 15767	Extend class notation to include the subset relation for subcategories.
class C_cat
Syntax	cresc 15768	Extend class notation to include category restriction (which is like structure restriction but also allows limiting the collection of morphisms).
class |`cat
Syntax	csubc 15769	Extend class notation to include the collection of subcategories of a category.
class Subcat
Definition	df-ssc 15770*	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 15772, 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 15771*	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 15772*	(Subcat ` C ) is the set of all the subcategory specifications of the category C. Like df-subg 16869, 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 15771) 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 15773	The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Rel C_cat
Theorem	brssc 15774*	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 15775*	An analogue of pwex 4603 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 15776	Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- ( H e. (Subcat ` C ) -> C e. Cat )
Theorem	sscfn1 15777	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 15778	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 15779	Lemma for ssc1 15781 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 15780*	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 15781	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 15782	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 15783	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 15784	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 15785	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 15786	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 15787	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 15788	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 15789	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 15790	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 15791	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 15792	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 15793	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 15794	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 15795*	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 15796*	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 15797	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 15798	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 15799	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 15800	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 )