P. 167 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16601-16700   *Has distinct variable group(s)

Type	Label	Description
Statement
8.1.9  Natural transformations and the functor category
Syntax	cnat 16601	Extend class notation to include the collection of natural transformations.
class Nat
Syntax	cfuc 16602	Extend class notation to include the functor category.
class FuncCat
Definition	df-nat 16603*	Definition of a natural transformation between two functors. A natural transformation A : F --> G is a collection of arrows A ( x ) : F ( x ) --> G ( x ), such that A ( y ) o. F ( h ) = G ( h ) o. A ( x ) for each morphism h : x --> y. Definition 6.1 in [Adamek] p. 83, and definition in [Lang] p. 65. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Nat = ( t e. Cat , u e. Cat |-> ( f e. ( t Func u ) , g e. ( t Func u ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` t ) ( ( r ` x ) ( Hom ` u ) ( s ` x ) ) | A. x e. ( Base ` t ) A. y e. ( Base ` t ) A. h e. ( x ( Hom ` t ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. (comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. (comp ` u ) ( s ` y ) ) ( a ` x ) ) } ) )
Definition	df-fuc 16604*	Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- FuncCat = ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. (comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. (comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )
Theorem	fnfuc 16605	The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- FuncCat Fn ( Cat X. Cat )
Theorem	natfval 16606*	Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- N = ( C Nat D )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- .x. = (comp ` D )   =>    |- N = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. B ( ( r ` x ) J ( s ` x ) ) | A. x e. B A. y e. B A. h e. ( x H y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. .x. ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. .x. ( s ` y ) ) ( a ` x ) ) } )
Theorem	isnat 16607*	Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- N = ( C Nat D )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- .x. = (comp ` D )   &    |- ( ph -> F ( C Func D ) G )   &    |- ( ph -> K ( C Func D ) L )   =>    |- ( ph -> ( A e. ( <. F , G >. N <. K , L >. ) <-> ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) ) ) )
Theorem	isnat2 16608*	Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- N = ( C Nat D )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- .x. = (comp ` D )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func D ) )   =>    |- ( ph -> ( A e. ( F N G ) <-> ( A e. X_ x e. B ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. .x. ( ( 1st ` G ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` h ) ) = ( ( ( x ( 2nd ` G ) y ) ` h ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` G ) ` y ) ) ( A ` x ) ) ) ) )
Theorem	natffn 16609	The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- N = ( C Nat D )   =>    |- N Fn ( ( C Func D ) X. ( C Func D ) )
Theorem	natrcl 16610	Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- N = ( C Nat D )   =>    |- ( A e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
Theorem	nat1st2nd 16611	Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- N = ( C Nat D )   &    |- ( ph -> A e. ( F N G ) )   =>    |- ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
Theorem	natixp 16612*	A natural transformation is a function from the objects of C to homomorphisms from F ( x ) to G ( x ). (Contributed by Mario Carneiro, 6-Jan-2017.)
|- N = ( C Nat D )   &    |- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )   &    |- B = ( Base ` C )   &    |- J = ( Hom ` D )   =>    |- ( ph -> A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) )
Theorem	natcl 16613	A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- N = ( C Nat D )   &    |- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )   &    |- B = ( Base ` C )   &    |- J = ( Hom ` D )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( A ` X ) e. ( ( F ` X ) J ( K ` X ) ) )
Theorem	natfn 16614	A natural transformation is a function on the objects of C. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- N = ( C Nat D )   &    |- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )   &    |- B = ( Base ` C )   =>    |- ( ph -> A Fn B )
Theorem	nati 16615	Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- N = ( C Nat D )   &    |- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` D )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> R e. ( X H Y ) )   =>    |- ( ph -> ( ( A ` Y ) ( <. ( F ` X ) , ( F ` Y ) >. .x. ( K ` Y ) ) ( ( X G Y ) ` R ) ) = ( ( ( X L Y ) ` R ) ( <. ( F ` X ) , ( K ` X ) >. .x. ( K ` Y ) ) ( A ` X ) ) )
Theorem	wunnat 16616	A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- ( ph -> U e. WUni )   &    |- ( ph -> C e. U )   &    |- ( ph -> D e. U )   =>    |- ( ph -> ( C Nat D ) e. U )
Theorem	catstr 16617	A category structure is a structure. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } Struct <. 1 , ; 1 5 >.
Theorem	fucval 16618*	Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- B = ( C Func D )   &    |- N = ( C Nat D )   &    |- A = ( Base ` C )   &    |- .x. = (comp ` D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> .xb = ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) )   =>    |- ( ph -> Q = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , N >. , <. (comp ` ndx ) , .xb >. } )
Theorem	fuccofval 16619*	Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- B = ( C Func D )   &    |- N = ( C Nat D )   &    |- A = ( Base ` C )   &    |- .x. = (comp ` D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- .xb = (comp ` Q )   =>    |- ( ph -> .xb = ( v e. ( B X. B ) , h e. B |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g N h ) , a e. ( f N g ) |-> ( x e. A |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. .x. ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) )
Theorem	fucbas 16620	The objects of the functor category are functors from C to D. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 12-Jan-2017.)
|- Q = ( C FuncCat D )   =>    |- ( C Func D ) = ( Base ` Q )
Theorem	fuchom 16621	The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- N = ( C Nat D )   =>    |- N = ( Hom ` Q )
Theorem	fucco 16622*	Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- N = ( C Nat D )   &    |- A = ( Base ` C )   &    |- .x. = (comp ` D )   &    |- .xb = (comp ` Q )   &    |- ( ph -> R e. ( F N G ) )   &    |- ( ph -> S e. ( G N H ) )   =>    |- ( ph -> ( S ( <. F , G >. .xb H ) R ) = ( x e. A |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )
Theorem	fuccoval 16623	Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- N = ( C Nat D )   &    |- A = ( Base ` C )   &    |- .x. = (comp ` D )   &    |- .xb = (comp ` Q )   &    |- ( ph -> R e. ( F N G ) )   &    |- ( ph -> S e. ( G N H ) )   &    |- ( ph -> X e. A )   =>    |- ( ph -> ( ( S ( <. F , G >. .xb H ) R ) ` X ) = ( ( S ` X ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. .x. ( ( 1st ` H ) ` X ) ) ( R ` X ) ) )
Theorem	fuccocl 16624	The composition of two natural transformations is a natural transformation. Remark 6.14(a) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- N = ( C Nat D )   &    |- .xb = (comp ` Q )   &    |- ( ph -> R e. ( F N G ) )   &    |- ( ph -> S e. ( G N H ) )   =>    |- ( ph -> ( S ( <. F , G >. .xb H ) R ) e. ( F N H ) )
Theorem	fucidcl 16625	The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- N = ( C Nat D )   &    |- .1. = ( Id ` D )   &    |- ( ph -> F e. ( C Func D ) )   =>    |- ( ph -> ( .1. o. ( 1st ` F ) ) e. ( F N F ) )
Theorem	fuclid 16626	Left identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- N = ( C Nat D )   &    |- .xb = (comp ` Q )   &    |- .1. = ( Id ` D )   &    |- ( ph -> R e. ( F N G ) )   =>    |- ( ph -> ( ( .1. o. ( 1st ` G ) ) ( <. F , G >. .xb G ) R ) = R )
Theorem	fucrid 16627	Right identity of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- N = ( C Nat D )   &    |- .xb = (comp ` Q )   &    |- .1. = ( Id ` D )   &    |- ( ph -> R e. ( F N G ) )   =>    |- ( ph -> ( R ( <. F , F >. .xb G ) ( .1. o. ( 1st ` F ) ) ) = R )
Theorem	fucass 16628	Associativity of natural transformation composition. Remark 6.14(b) in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- N = ( C Nat D )   &    |- .xb = (comp ` Q )   &    |- ( ph -> R e. ( F N G ) )   &    |- ( ph -> S e. ( G N H ) )   &    |- ( ph -> T e. ( H N K ) )   =>    |- ( ph -> ( ( T ( <. G , H >. .xb K ) S ) ( <. F , G >. .xb K ) R ) = ( T ( <. F , H >. .xb K ) ( S ( <. F , G >. .xb H ) R ) ) )
Theorem	fuccatid 16629*	The functor category is a category. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- .1. = ( Id ` D )   =>    |- ( ph -> ( Q e. Cat /\ ( Id ` Q ) = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) ) )
Theorem	fuccat 16630	The functor category is a category. Remark 6.16 in [Adamek] p. 88. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> Q e. Cat )
Theorem	fucid 16631	The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- I = ( Id ` Q )   &    |- .1. = ( Id ` D )   &    |- ( ph -> F e. ( C Func D ) )   =>    |- ( ph -> ( I ` F ) = ( .1. o. ( 1st ` F ) ) )
Theorem	fucsect 16632*	Two natural transformations are in a section iff all the components are in a section relation. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- B = ( Base ` C )   &    |- N = ( C Nat D )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func D ) )   &    |- S = (Sect ` Q )   &    |- T = (Sect ` D )   =>    |- ( ph -> ( U ( F S G ) V <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) T ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) )
Theorem	fucinv 16633*	Two natural transformations are inverses of each other iff all the components are inverse. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- B = ( Base ` C )   &    |- N = ( C Nat D )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func D ) )   &    |- I = (Inv ` Q )   &    |- J = (Inv ` D )   =>    |- ( ph -> ( U ( F I G ) V <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) )
Theorem	invfuc 16634*	If V ( x ) is an inverse to U ( x ) for each x, and U is a natural transformation, then V is also a natural transformation, and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- B = ( Base ` C )   &    |- N = ( C Nat D )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func D ) )   &    |- I = (Inv ` Q )   &    |- J = (Inv ` D )   &    |- ( ph -> U e. ( F N G ) )   &    |- ( ( ph /\ x e. B ) -> ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) X )   =>    |- ( ph -> U ( F I G ) ( x e. B |-> X ) )
Theorem	fuciso 16635*	A natural transformation is an isomorphism of functors iff all its components are isomorphisms. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- Q = ( C FuncCat D )   &    |- B = ( Base ` C )   &    |- N = ( C Nat D )   &    |- ( ph -> F e. ( C Func D ) )   &    |- ( ph -> G e. ( C Func D ) )   &    |- I = ( Iso ` Q )   &    |- J = ( Iso ` D )   =>    |- ( ph -> ( A e. ( F I G ) <-> ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) )
Theorem	natpropd 16636	If two categories have the same set of objects, morphisms, and compositions, then they have the same natural transformations. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> ( Hom f ` A ) = ( Hom f ` B ) )   &    |- ( ph -> (compf ` A ) = (compf ` B ) )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> A e. Cat )   &    |- ( ph -> B e. Cat )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> ( A Nat C ) = ( B Nat D ) )
Theorem	fucpropd 16637	If two categories have the same set of objects, morphisms, and compositions, then they have the same functor categories. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> ( Hom f ` A ) = ( Hom f ` B ) )   &    |- ( ph -> (compf ` A ) = (compf ` B ) )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> A e. Cat )   &    |- ( ph -> B e. Cat )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> ( A FuncCat C ) = ( B FuncCat D ) )
8.1.10  Initial, terminal and zero objects of a category
Syntax	cinito 16638	Extend class notation with the class of initial objects of a category.
class InitO
Syntax	ctermo 16639	Extend class notation with the class of terminal objects of a category.
class TermO
Syntax	czeroo 16640	Extend class notation with the class of zero objects of a category.
class ZeroO
Definition	df-inito 16641*	An object A is said to be an initial object provided that for each object B there is exactly one morphism from A to B. Definition 7.1 in [Adamek] p. 101, or definition in [Lang] p. 57 (called "a universally repelling object" there). (Contributed by AV, 3-Apr-2020.)
|- InitO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } )
Definition	df-termo 16642*	An object A is called a terminal object provided that for each object B there is exactly one morphism from B to A. Definition 7.4 in [Adamek] p. 102, or definition in [Lang] p. 57 (called "a universally attracting object" there). (Contributed by AV, 3-Apr-2020.)
|- TermO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )
Definition	df-zeroo 16643	An object A is called a zero object provided that it is both an initial object and a terminal object. Definition 7.7 of [Adamek] p. 103. (Contributed by AV, 3-Apr-2020.)
|- ZeroO = ( c e. Cat |-> ( (InitO ` c ) i^i (TermO ` c ) ) )
Theorem	initorcl 16644	Reverse closure for an initial object: If a class has an initial object, the class is a category. (Contributed by AV, 4-Apr-2020.)
|- ( I e. (InitO ` C ) -> C e. Cat )
Theorem	termorcl 16645	Reverse closure for a terminal object: If a class has a terminal object, the class is a category. (Contributed by AV, 4-Apr-2020.)
|- ( T e. (TermO ` C ) -> C e. Cat )
Theorem	zeroorcl 16646	Reverse closure for a zero object: If a class has a zero object, the class is a category. (Contributed by AV, 4-Apr-2020.)
|- ( Z e. (ZeroO ` C ) -> C e. Cat )
Theorem	initoval 16647*	The value of the initial object function, i.e. the set of all initial objects of a category. (Contributed by AV, 3-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   =>    |- ( ph -> (InitO ` C ) = { a e. B | A. b e. B E! h h e. ( a H b ) } )
Theorem	termoval 16648*	The value of the terminal object function, i.e. the set of all terminal objects of a category. (Contributed by AV, 3-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   =>    |- ( ph -> (TermO ` C ) = { a e. B | A. b e. B E! h h e. ( b H a ) } )
Theorem	zerooval 16649	The value of the zero object function, i.e. the set of all zero objects of a category. (Contributed by AV, 3-Apr-2020.)
|- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   =>    |- ( ph -> (ZeroO ` C ) = ( (InitO ` C ) i^i (TermO ` C ) ) )
Theorem	isinito 16650*	The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> I e. B )   =>    |- ( ph -> ( I e. (InitO ` C ) <-> A. b e. B E! h h e. ( I H b ) ) )
Theorem	istermo 16651*	The predicate "is a terminal object" of a category. (Contributed by AV, 3-Apr-2020.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> I e. B )   =>    |- ( ph -> ( I e. (TermO ` C ) <-> A. b e. B E! h h e. ( b H I ) ) )
Theorem	iszeroo 16652	The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> I e. B )   =>    |- ( ph -> ( I e. (ZeroO ` C ) <-> ( I e. (InitO ` C ) /\ I e. (TermO ` C ) ) ) )
Theorem	isinitoi 16653*	Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   =>    |- ( ( ph /\ O e. (InitO ` C ) ) -> ( O e. B /\ A. b e. B E! h h e. ( O H b ) ) )
Theorem	istermoi 16654*	Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   =>    |- ( ( ph /\ O e. (TermO ` C ) ) -> ( O e. B /\ A. b e. B E! h h e. ( b H O ) ) )
Theorem	initoid 16655	For an initial object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 6-Apr-2020.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   =>    |- ( ( ph /\ O e. (InitO ` C ) ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } )
Theorem	termoid 16656	For a terminal object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 18-Apr-2020.)
|- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   =>    |- ( ( ph /\ O e. (TermO ` C ) ) -> ( O H O ) = { ( ( Id ` C ) ` O ) } )
Theorem	initoo 16657	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 16658	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 16659	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 16660	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 16661*	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 16662	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 16663	Lemma 0 for initoeu2 16666. (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 16664*	Lemma 1 for initoeu2 16666. (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 16665*	Lemma 2 for initoeu2 16666. (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 16666	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 16667	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 16668*	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 16669	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 16670	Extend class notation to include the domain extractor for an arrow.
class domA
Syntax	ccoda 16671	Extend class notation to include the codomain extractor for an arrow.
class coda
Syntax	carw 16672	Extend class notation to include the collection of all arrows of a category.
class Nat
Syntax	choma 16673	Extend class notation to include the set of all arrows with a specific domain and codomain.
class Homa
Definition	df-doma 16674	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 16675	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 16676*	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 16674 and df-coda 16675. (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 16677	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 16678	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 16679*	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 16680	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 16681	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 16682	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 16683	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 16684	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 16685	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 16686	An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   =>    |- Rel ( X H Y )
Theorem	homa1 16687	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 16688	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 16689	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 16690	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 16691	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 16692	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 16693	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 16694	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 16695	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 16696	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 16697	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 16698	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 16699	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 16700	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