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
8.1.9  Natural transformations and the functor category
Syntax	cnat 15901	Extend class notation to include the collection of natural transformations.
class Nat
Syntax	cfuc 15902	Extend class notation to include the functor category.
class FuncCat
Definition	df-nat 15903*	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 15904*	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 15905	The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- FuncCat Fn ( Cat X. Cat )
Theorem	natfval 15906*	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 15907*	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 15908*	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 15909	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 15910	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 15911	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 15912*	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 15913	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 15914	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 15915	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 15916	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 15917	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 15918*	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 15919*	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 15920	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 15921	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 15922*	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 15923	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 15924	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 15925	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 15926	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 15927	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 15928	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 15929*	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 15930	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 15931	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 15932*	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 15933*	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 15934*	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 15935*	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 15936	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 15937	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 15938	Extend class notation with the class of initial objects of a category.
class InitO
Syntax	ctermo 15939	Extend class notation with the class of terminal objects of a category.
class TermO
Syntax	czeroo 15940	Extend class notation with the class of zero objects of a category.
class ZeroO
Definition	df-inito 15941*	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 15942*	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 15943	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 15944	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 15945	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 15946	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 15947*	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 15948*	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 15949	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 15950*	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 15951*	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 15952	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 15953*	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 15954*	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 15955	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 15956	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 15957	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 15958	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 15959	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 15960	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 15961*	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 15962	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 15963	Lemma 0 for initoeu2 15966. (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 15964*	Lemma 1 for initoeu2 15966. (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 15965*	Lemma 2 for initoeu2 15966. (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 15966	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 15967	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 15968*	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 15969	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 15970	Extend class notation to include the domain extractor for an arrow.
class domA
Syntax	ccoda 15971	Extend class notation to include the codomain extractor for an arrow.
class coda
Syntax	carw 15972	Extend class notation to include the collection of all arrows of a category.
class Nat
Syntax	choma 15973	Extend class notation to include the set of all arrows with a specific domain and codomain.
class Homa
Definition	df-doma 15974	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 15975	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 15976*	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 15974 and df-coda 15975. (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 15977	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 15978	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 15979*	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 15980	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 15981	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 15982	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 15983	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 15984	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 15985	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 15986	An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   =>    |- Rel ( X H Y )
Theorem	homa1 15987	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 15988	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 15989	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 15990	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 15991	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 15992	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 15993	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 15994	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 15995	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 15996	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 15997	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 15998	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 15999	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 16000	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