P. 160 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	coafval 15901*	The value of the composition of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- A = (Nat ` C )   &    |- .xb = (comp ` C )   =>    |- .x. = ( g e. A , f e. { h e. A | (coda ` h ) = (domA ` g ) } |-> <. (domA ` f ) , (coda ` g ) , ( ( 2nd ` g ) ( <. (domA ` f ) , (domA ` g ) >. .xb (coda ` g ) ) ( 2nd ` f ) ) >. )
Theorem	eldmcoa 15902	A pair <. G , F >. is in the domain of the arrow composition, if the domain of G equals the codomain of F. (In this case we say G and F are composable.) (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- A = (Nat ` C )   =>    |- ( G dom .x. F <-> ( F e. A /\ G e. A /\ (coda ` F ) = (domA ` G ) ) )
Theorem	dmcoass 15903	The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- A = (Nat ` C )   =>    |- dom .x. C_ ( A X. A )
Theorem	homdmcoa 15904	If F : X --> Y and G : Y --> Z, then G and F are composable. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- H = (Homa ` C )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   =>    |- ( ph -> G dom .x. F )
Theorem	coaval 15905	Value of composition for composable arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- H = (Homa ` C )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   &    |- .xb = (comp ` C )   =>    |- ( ph -> ( G .x. F ) = <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) >. )
Theorem	coa2 15906	The morphism part of arrow composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- H = (Homa ` C )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   &    |- .xb = (comp ` C )   =>    |- ( ph -> ( 2nd ` ( G .x. F ) ) = ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) )
Theorem	coahom 15907	The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- H = (Homa ` C )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   =>    |- ( ph -> ( G .x. F ) e. ( X H Z ) )
Theorem	coapm 15908	Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- .x. = (compa ` C )   &    |- A = (Nat ` C )   =>    |- .x. e. ( A ^pm ( A X. A ) )
Theorem	arwlid 15909	Left identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- .x. = (compa ` C )   &    |- .1. = (Ida ` C )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( ( .1. ` Y ) .x. F ) = F )
Theorem	arwrid 15910	Right identity of a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- .x. = (compa ` C )   &    |- .1. = (Ida ` C )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( F .x. ( .1. ` X ) ) = F )
Theorem	arwass 15911	Associativity of composition in a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- H = (Homa ` C )   &    |- .x. = (compa ` C )   &    |- .1. = (Ida ` C )   &    |- ( ph -> F e. ( X H Y ) )   &    |- ( ph -> G e. ( Y H Z ) )   &    |- ( ph -> K e. ( Z H W ) )   =>    |- ( ph -> ( ( K .x. G ) .x. F ) = ( K .x. ( G .x. F ) ) )
8.3  Examples of categories
8.3.1  The category of sets
Syntax	csetc 15912	Extend class notation to include the category Set.
class SetCat
Definition	df-setc 15913*	Definition of the category Set, relativized to a subset u. Example 3.3(1) of [Adamek] p. 22. This is the category of all sets in u and functions between these sets. Generally, we will take u to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by FL, 8-Nov-2013.) (Revised by Mario Carneiro, 3-Jan-2017.)
|- SetCat = ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( y ^m x ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. } )
Theorem	setcval 15914*	Value of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> H = ( x e. U , y e. U |-> ( y ^m x ) ) )   &    |- ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	setcbas 15915	Set of objects of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   =>    |- ( ph -> U = ( Base ` C ) )
Theorem	setchomfval 15916*	Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. U , y e. U |-> ( y ^m x ) ) )
Theorem	setchom 15917	Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( X H Y ) = ( Y ^m X ) )
Theorem	elsetchom 15918	A morphism of sets is a function. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( F e. ( X H Y ) <-> F : X --> Y ) )
Theorem	setccofval 15919*	Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) )
Theorem	setcco 15920	Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- ( ph -> Z e. U )   &    |- ( ph -> F : X --> Y )   &    |- ( ph -> G : Y --> Z )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )
Theorem	setccatid 15921*	Lemma for setccat 15922. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` x ) ) ) )
Theorem	setccat 15922	The category of sets is a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	setcid 15923	The identity arrow in the category of sets is the identity function. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` X ) )
Theorem	setcmon 15924	A monomorphism of sets is an injection. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- M = (Mono ` C )   =>    |- ( ph -> ( F e. ( X M Y ) <-> F : X -1-1-> Y ) )
Theorem	setcepi 15925	An epimorphism of sets is a surjection. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- E = (Epi ` C )   &    |- ( ph -> 2o e. U )   =>    |- ( ph -> ( F e. ( X E Y ) <-> F : X -onto-> Y ) )
Theorem	setcsect 15926	A section in the category of sets, written out. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- S = (Sect ` C )   =>    |- ( ph -> ( F ( X S Y ) G <-> ( F : X --> Y /\ G : Y --> X /\ ( G o. F ) = ( _I |` X ) ) ) )
Theorem	setcinv 15927	An inverse in the category of sets is the converse operation. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- N = (Inv ` C )   =>    |- ( ph -> ( F ( X N Y ) G <-> ( F : X -1-1-onto-> Y /\ G = `' F ) ) )
Theorem	setciso 15928	An isomorphism in the category of sets is a bijection. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( F e. ( X I Y ) <-> F : X -1-1-onto-> Y ) )
Theorem	resssetc 15929	The restriction of the category of sets to a subset is the category of sets in the subset. Thus, the SetCat ` U categories for different U are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- C = ( SetCat ` U )   &    |- D = ( SetCat ` V )   &    |- ( ph -> U e. W )   &    |- ( ph -> V C_ U )   =>    |- ( ph -> ( ( Hom f ` ( C ↾s V ) ) = ( Hom f ` D ) /\ (compf ` ( C ↾s V ) ) = (compf ` D ) ) )
Theorem	funcsetcres2 15930	A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- C = ( SetCat ` U )   &    |- D = ( SetCat ` V )   &    |- ( ph -> U e. W )   &    |- ( ph -> V C_ U )   =>    |- ( ph -> ( E Func D ) C_ ( E Func C ) )
8.3.2  The category of categories
Syntax	ccatc 15931	Extend class notation to include the category Cat.
class CatCat
Definition	df-catc 15932*	Definition of the category Cat, which consists of all categories in the universe u (i.e. "small categories", see definition 3.44. of [Adamek] p. 39), with functors as the morphisms. Definition 3.47 of [Adamek] p. 40. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- CatCat = ( u e. _V |-> [_ ( u i^i Cat ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x Func y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) >. } )
Theorem	catcval 15933*	Value of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Cat ) )   &    |- ( ph -> H = ( x e. B , y e. B |-> ( x Func y ) ) )   &    |- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	catcbas 15934	Set of objects of the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Cat ) )
Theorem	catchomfval 15935*	Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. B , y e. B |-> ( x Func y ) ) )
Theorem	catchom 15936	Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X Func Y ) )
Theorem	catccofval 15937*	Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) )
Theorem	catcco 15938	Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( X Func Y ) )   &    |- ( ph -> G e. ( Y Func Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o.func F ) )
Theorem	catccatid 15939*	Lemma for catccat 15941. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> (idfunc ` x ) ) ) )
Theorem	catcid 15940	The identity arrow in the category of categories is the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- I = (idfunc ` X )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( .1. ` X ) = I )
Theorem	catccat 15941	The category of categories is a category, see remark 3.48 in [Adamek] p. 40. (Clearly it cannot be an element of itself, hence it is "large" with respect to U.) (Contributed by Mario Carneiro, 3-Jan-2017.)
|- C = (CatCat ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	resscatc 15942	The restriction of the category of categories to a subset is the category of categories in the subset. Thus, the CatCat ` U categories for different U are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017.)
|- C = (CatCat ` U )   &    |- D = (CatCat ` V )   &    |- ( ph -> U e. W )   &    |- ( ph -> V C_ U )   =>    |- ( ph -> ( ( Hom f ` ( C ↾s V ) ) = ( Hom f ` D ) /\ (compf ` ( C ↾s V ) ) = (compf ` D ) ) )
Theorem	catcisolem 15943*	Lemma for catciso 15944. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- R = ( Base ` X )   &    |- S = ( Base ` Y )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = (Inv ` C )   &    |- H = ( x e. S , y e. S |-> `' ( ( `' F ` x ) G ( `' F ` y ) ) )   &    |- ( ph -> F ( ( X Full Y ) i^i ( X Faith Y ) ) G )   &    |- ( ph -> F : R -1-1-onto-> S )   =>    |- ( ph -> <. F , G >. ( X I Y ) <. `' F , H >. )
Theorem	catciso 15944	A functor is an isomorphism of categories if and only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in [Adamek] p. 34. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- R = ( Base ` X )   &    |- S = ( Base ` Y )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( F e. ( X I Y ) <-> ( F e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` F ) : R -1-1-onto-> S ) ) )
Theorem	catcoppccl 15945	The category of categories for a weak universe is closed under taking opposites. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- O = (oppCat ` X )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> X e. B )   =>    |- ( ph -> O e. B )
Theorem	catcfuccl 15946	The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- C = (CatCat ` U )   &    |- B = ( Base ` C )   &    |- Q = ( X FuncCat Y )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> Q e. B )
8.3.3  The category of extensible structures The "category of extensible structures" ExtStrCat is the category of all sets in a universe regarded as extensible structures and the functions between their base sets, see df-estrc 15950. Since we consider only "small categories" (i.e. categories whose objects and morphisms are actually sets and not proper classes), the objects of the category (i.e. the base set of the category regarded as extensible structure) are all sets in a universe u, which can be an arbitrary set, see estrcbas 15952. Generally, we will take u to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. If a set is not a real extensible structure, it is regarded as extensible structure with an empty base set. Because of bascnvimaeqv 15948 we do not need to restrict the universe to sets which "have a base". The morphisms (or arrows) between two objects, i.e. sets from the universe, are the mappings between their base sets, see estrchomfval 15953, whereas the composition is the ordinary composition of functions, see estrccofval 15956 and estrcco 15957. It is shown that the category of extensible structures ExtStrCat is actually a category, see estrccat 15960 with the identity function as identity arrow, see estrcid 15961. In the following, some background information about the category of extensible structures is given, taken from the discussion in Github issue #1507 (see https://github.com/metamath/set.mm/issues/1507): At the beginning, the categories of non-unital rings RngCat and unital rings RingCat were defined separately (as unordered triples of ordereds pairs, see dfrngc2 38722 and dfringc2 38768, but with special compositions). With this definitions, however, theorem rngcresringcat 38780 could not be proven, because the compositions were not compatible. Unfortunately, no precise definition of the composition within the category of rings could be found in the literature. In section 3.3 EXAMPLES, paragraph (2) of [Adamek] p. 22, however, a definition is given for "Grp", the category of groups: "The following constructs; i.e., categories of structured sets and structure-preserving functions between them (o will always be the composition of functions and idA will always be the identity function on A): ... (b) Grp with objects all groups and morphisms all homomorphisms between them." Therefore, the compositions should have been harmonized by using the composition of the category of sets SetCat, see df-setc 15913, which is the ordinary composition of functions. Analogously, categories of Rngs (and Rings) could have been shown to be restrictions resp. subcategories of the category of sets. BJ and MC observed, however, that "... |`cat [cannot be used] to restrict the category Set to Ring, because the homs are different. Although Ring is a concrete category, a hom between rings R and S is a function (Base`R) --> (Base`S) with certain properties, unlike in Set where it is a function R --> S.". Therefore, MC suggested that "we could have an alternative version of the Set category consisting of extensible structures (in U) together with (A Hom B) := (Base`A) --> (Base`B). This category is not isomorphic to Set because different extensible structures can have the same base set, but it is equivalent to Set; the relevant functors are (U`A) = (Base`A), the forgetful functor, and (F`A) = { <. (Base`ndx), A >. }". This led to the current definition of ExtStrCat, see df-estrc 15950. The claimed equivalence is proven by equivestrcsetc 15979. Having a definition of a category of extensible structures, the categories of non-unital and unital rings can be defined as appropriate restrictions of the category of extensible structures, see df-rngc 38709 and df-ringc 38755. In the same way, more subcategories could be provided, resulting in the following "inclusion chain" by proving theorems like rngcresringcat 38780, although the morphisms of the shown categories are different ( "->" means "is subcategory of"): RingCat-> RngCat-> GrpCat -> MndCat -> MgmCat -> ExtStrCat According to MC, "If we generalize from subcategories to embeddings, then we can even fit SetCat into the chain, equivalent to ExtStrCat at the end." As mentioned before, the equivalence of SetCat and ExtStrCat is proven by equivestrcsetc 15979. Furthermore, it can be shown that SetCat is embedded into ExtStrCat, see embedsetcestrc 15994. Remark: equivestrcsetc 15979 as well as embedsetcestrc 15994 require that the index of the base set extractor is contained within the considered universe. This is assured by assuming that the natural numbers are contained within the considered universe: om e. U (see wunndx 15091), but it would be currently sufficient to assume that 1 e. U, because the index value of the base set extractor is hard-coded as 1, see basendx 15127. Some people, however, feel uncomfortable to say that a ring "is a" group (without mentioning the restriction to the addition, which is usually found in the literature, e.g. the definition of a ring in [Herstein] p. 126: "... Note that so far all we have said is that R is an abelian group under +.". The main argument against a ring being a group is the number of components/slots: usually, a group consists of (exactly!) two components (a base set and an operation), whereas a ring consists of (exactly!) three components (a base set and two operations). According to this "definition", a ring cannot be a group. This is also an (unfortunately informal) argument for the category of rings not being a subcategory of the category of abelian groups in "Categories and Functors", Bodo Pareigis, Academic Press, New York, London, 1970: "A category A is called a subcategory of a category B if Ob(A) C_ Ob(B) and MorA(X,Y) C_ MorB(X,Y) for all X,Y e. Ob(A), if the composition of morphisms in A coincides with the composition of the same morphisms in B and if the identity of an object in A is also the identity of the same object viewed as an object in B. Then there is a forgetful functor from A to B. We note that Ri [the category of rings] is not a subcategory of Ab [the category of abelian groups]. In fact, Ob(Ri) C_ Ob(Ab) is not true, although every ring can also be regarded as an abelian group. The corresponding abelian groups of two rings may coincide even if the rings do not coincide. The multiplication may be defined differently.". As long as we define Rings, Groups, etc. in a way that A e. Ring -> A e. Grp is valid (see ringgrp 17711) the corresponding categories are in a subcategory relation. If we do not want Rings to be Groups (then the category of rings would not be a subcategory of the category of groups, as observed by Pareigis), we would have to change the definitions of Magmas, Monoids, Groups, Rings etc. to restrict them to have exactly the required number of slots, so that the following holds g e. Grp -> g Struct <. ( Base ` ndx ) , ( +g ` ndx ) >. r e. Ring -> r Struct <. ( Base ` ndx ) , ( +g ` ndx ) , ( .r ndx ) >.
Theorem	fncnvimaeqv 15947	The inverse images of the universal class _V under functions on the universal class _V are the universal class _V itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020.)
|- ( F Fn _V -> ( `' F " _V ) = _V )
Theorem	bascnvimaeqv 15948	The inverse image of the universal class _V under the base function is the universal class _V itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020.)
|- ( `' Base " _V ) = _V
Syntax	cestrc 15949	Extend class notation to include the category ExtStr.
class ExtStrCat
Definition	df-estrc 15950*	Definition of the category ExtStr of extensible structures. This is the category whose objects are all sets in a universe u regarded as extensible structures and whose morphisms are the functions between their base sets. If a set is not a real extensible structure, it is regarded as extensible structure with an empty base set. Because of bascnvimaeqv 15948 we do not need to restrict the universe to sets which "have a base". Generally, we will take u to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Proposed by Mario Carneiro, 5-Mar-2020.) (Contributed by AV, 7-Mar-2020.)
|- ExtStrCat = ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) >. } )
Theorem	estrcval 15951*	Value of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> H = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )   &    |- ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	estrcbas 15952	Set of objects of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   =>    |- ( ph -> U = ( Base ` C ) )
Theorem	estrchomfval 15953*	Set of morphisms ("arrows") of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
Theorem	estrchom 15954	The morphisms between extensible structures are mappings between their base sets. (Contributed by AV, 7-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- A = ( Base ` X )   &    |- B = ( Base ` Y )   =>    |- ( ph -> ( X H Y ) = ( B ^m A ) )
Theorem	elestrchom 15955	A morphism between extensible structures is a function between their base sets. (Contributed by AV, 7-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- A = ( Base ` X )   &    |- B = ( Base ` Y )   =>    |- ( ph -> ( F e. ( X H Y ) <-> F : A --> B ) )
Theorem	estrccofval 15956*	Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) )
Theorem	estrcco 15957	Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- ( ph -> Z e. U )   &    |- A = ( Base ` X )   &    |- B = ( Base ` Y )   &    |- D = ( Base ` Z )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> G : B --> D )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )
Theorem	estrcbasbas 15958	An element of the base set of the base set of the category of extensible structures (i.e. the base set of an extensible structure) belongs to the considered weak universe. (Contributed by AV, 22-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. WUni )   =>    |- ( ( ph /\ E e. B ) -> ( Base ` E ) e. U )
Theorem	estrccatid 15959*	Lemma for estrccat 15960. (Contributed by AV, 8-Mar-2020.)
|- C = (ExtStrCat ` U )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` ( Base ` x ) ) ) ) )
Theorem	estrccat 15960	The category of extensible structures is a category. (Contributed by AV, 8-Mar-2020.)
|- C = (ExtStrCat ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	estrcid 15961	The identity arrow in the category of extensible structures is the identity function of base sets. (Contributed by AV, 8-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. U )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` ( Base ` X ) ) )
Theorem	estrchomfn 15962	The Hom-set operation in the category of extensible structures (in a universe) is a function. (Contributed by AV, 8-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H Fn ( U X. U ) )
Theorem	estrchomfeqhom 15963	The functionalized Hom-set operation equals the Hom-set operation in the category of extensible structures (in a universe). (Contributed by AV, 8-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> ( Hom f ` C ) = H )
Theorem	estrreslem1 15964	Lemma 1 for estrres 15966. (Contributed by AV, 14-Mar-2020.)
|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   =>    |- ( ph -> B = ( Base ` C ) )
Theorem	estrreslem2 15965	Lemma 2 for estrres 15966. (Contributed by AV, 14-Mar-2020.)
|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> H e. X )   &    |- ( ph -> .x. e. Y )   =>    |- ( ph -> ( Base ` ndx ) e. dom C )
Theorem	estrres 15966	Any restriction of a category (as an extensible structure which is an unordered triple of ordered pairs) is an unordered triple of ordered pairs. (Contributed by AV, 15-Mar-2020.)
|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> H e. X )   &    |- ( ph -> .x. e. Y )   &    |- ( ph -> A e. U )   &    |- ( ph -> G e. W )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> ( ( C ↾s A ) sSet <. ( Hom ` ndx ) , G >. ) = { <. ( Base ` ndx ) , A >. , <. ( Hom ` ndx ) , G >. , <. (comp ` ndx ) , .x. >. } )
Theorem	funcestrcsetclem1 15967*	Lemma 1 for funcestrcsetc 15976. (Contributed by AV, 22-Mar-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( F ` X ) = ( Base ` X ) )
Theorem	funcestrcsetclem2 15968*	Lemma 2 for funcestrcsetc 15976. (Contributed by AV, 22-Mar-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( F ` X ) e. U )
Theorem	funcestrcsetclem3 15969*	Lemma 3 for funcestrcsetc 15976. (Contributed by AV, 22-Mar-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ph -> F : B --> C )
Theorem	funcestrcsetclem4 15970*	Lemma 4 for funcestrcsetc 15976. (Contributed by AV, 22-Mar-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )   =>    |- ( ph -> G Fn ( B X. B ) )
Theorem	funcestrcsetclem5 15971*	Lemma 5 for funcestrcsetc 15976. (Contributed by AV, 23-Mar-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )   &    |- M = ( Base ` X )   &    |- N = ( Base ` Y )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) = ( _I |` ( N ^m M ) ) )
Theorem	funcestrcsetclem6 15972*	Lemma 6 for funcestrcsetc 15976. (Contributed by AV, 23-Mar-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )   &    |- M = ( Base ` X )   &    |- N = ( Base ` Y )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( N ^m M ) ) -> ( ( X G Y ) ` H ) = H )
Theorem	funcestrcsetclem7 15973*	Lemma 7 for funcestrcsetc 15976. (Contributed by AV, 23-Mar-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( ( X G X ) ` ( ( Id ` E ) ` X ) ) = ( ( Id ` S ) ` ( F ` X ) ) )
Theorem	funcestrcsetclem8 15974*	Lemma 8 for funcestrcsetc 15976. (Contributed by AV, 15-Feb-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) : ( X ( Hom ` E ) Y ) --> ( ( F ` X ) ( Hom ` S ) ( F ` Y ) ) )
Theorem	funcestrcsetclem9 15975*	Lemma 9 for funcestrcsetc 15976. (Contributed by AV, 23-Mar-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( H e. ( X ( Hom ` E ) Y ) /\ K e. ( Y ( Hom ` E ) Z ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. (comp ` E ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. (comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )
Theorem	funcestrcsetc 15976*	The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 23-Mar-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )   =>    |- ( ph -> F ( E Func S ) G )
Theorem	fthestrcsetc 15977*	The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is faithful. (Contributed by AV, 2-Apr-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )   =>    |- ( ph -> F ( E Faith S ) G )
Theorem	fullestrcsetc 15978*	The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is full. (Contributed by AV, 2-Apr-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )   =>    |- ( ph -> F ( E Full S ) G )
Theorem	equivestrcsetc 15979*	The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is an equivalence. According to definition 3.33 (1) of [Adamek] p. 36, "A functor F : A -> B is called an equivalence provided that it is full, faithful, and isomorphism-dense in the sense that for any B-object B' there exists some A-object A' such that F(A') is isomorphic to B'.". Therefore, the category of sets and the category of extensible structures are equivalent, according to definition 3.33 (2) of [Adamek] p. 36, "Categories A and B are called equivalent provided that there is an equivalence from A to B.". (Contributed by AV, 2-Apr-2020.)
|- E = (ExtStrCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` E )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )   &    |- ( ph -> ( Base ` ndx ) e. U )   =>    |- ( ph -> ( F ( E Faith S ) G /\ F ( E Full S ) G /\ A. b e. C E. a e. B E. i i : b -1-1-onto-> ( F ` a ) ) )
Theorem	setc1strwun 15980	A constructed one-slot structure with the objects of the category of sets as base set in a weak universe. (Contributed by AV, 27-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   =>    |- ( ( ph /\ X e. C ) -> { <. ( Base ` ndx ) , X >. } e. U )
Theorem	funcsetcestrclem1 15981*	Lemma 1 for funcsetcestrc 15991. (Contributed by AV, 27-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   =>    |- ( ( ph /\ X e. C ) -> ( F ` X ) = { <. ( Base ` ndx ) , X >. } )
Theorem	funcsetcestrclem2 15982*	Lemma 2 for funcsetcestrc 15991. (Contributed by AV, 27-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   =>    |- ( ( ph /\ X e. C ) -> ( F ` X ) e. U )
Theorem	funcsetcestrclem3 15983*	Lemma 3 for funcsetcestrc 15991. (Contributed by AV, 27-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- E = (ExtStrCat ` U )   &    |- B = ( Base ` E )   =>    |- ( ph -> F : C --> B )
Theorem	embedsetcestrclem 15984*	Lemma for embedsetcestrc 15994. (Contributed by AV, 31-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- E = (ExtStrCat ` U )   &    |- B = ( Base ` E )   =>    |- ( ph -> F : C -1-1-> B )
Theorem	funcsetcestrclem4 15985*	Lemma 4 for funcsetcestrc 15991. (Contributed by AV, 27-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   =>    |- ( ph -> G Fn ( C X. C ) )
Theorem	funcsetcestrclem5 15986*	Lemma 5 for funcsetcestrc 15991. (Contributed by AV, 27-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   =>    |- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X G Y ) = ( _I |` ( Y ^m X ) ) )
Theorem	funcsetcestrclem6 15987*	Lemma 6 for funcsetcestrc 15991. (Contributed by AV, 27-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   =>    |- ( ( ph /\ ( X e. C /\ Y e. C ) /\ H e. ( Y ^m X ) ) -> ( ( X G Y ) ` H ) = H )
Theorem	funcsetcestrclem7 15988*	Lemma 7 for funcsetcestrc 15991. (Contributed by AV, 27-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ( ph /\ X e. C ) -> ( ( X G X ) ` ( ( Id ` S ) ` X ) ) = ( ( Id ` E ) ` ( F ` X ) ) )
Theorem	funcsetcestrclem8 15989*	Lemma 8 for funcsetcestrc 15991. (Contributed by AV, 28-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X G Y ) : ( X ( Hom ` S ) Y ) --> ( ( F ` X ) ( Hom ` E ) ( F ` Y ) ) )
Theorem	funcsetcestrclem9 15990*	Lemma 9 for funcsetcestrc 15991. (Contributed by AV, 28-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ( ph /\ ( X e. C /\ Y e. C /\ Z e. C ) /\ ( H e. ( X ( Hom ` S ) Y ) /\ K e. ( Y ( Hom ` S ) Z ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. (comp ` S ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. (comp ` E ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )
Theorem	funcsetcestrc 15991*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 28-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ph -> F ( S Func E ) G )
Theorem	fthsetcestrc 15992*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is faithful. (Contributed by AV, 31-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ph -> F ( S Faith E ) G )
Theorem	fullsetcestrc 15993*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is full. (Contributed by AV, 1-Apr-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   =>    |- ( ph -> F ( S Full E ) G )
Theorem	embedsetcestrc 15994*	The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is an embedding. According to definition 3.27 (1) of [Adamek] p. 34, a functor "F is called an embedding provided that F is injective on morphisms", or according to remark 3.28 (1) in [Adamek] p. 34, "a functor is an embedding if and only if it is faithful and injective on objects". (Contributed by AV, 31-Mar-2020.)
|- S = ( SetCat ` U )   &    |- C = ( Base ` S )   &    |- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   &    |- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )   &    |- E = (ExtStrCat ` U )   &    |- B = ( Base ` E )   =>    |- ( ph -> ( F ( S Faith E ) G /\ F : C -1-1-> B ) )
8.4  Categorical constructions
8.4.1  Product of categories
Syntax	cxpc 15995	Extend class notation with the product of two categories.
class X.c
Syntax	c1stf 15996	Extend class notation with the first projection functor.
class 1stF
Syntax	c2ndf 15997	Extend class notation with the second projection functor.
class 2ndF
Syntax	cprf 15998	Extend class notation with the functor pairing operation.
class ⟨,⟩F
Definition	df-xpc 15999*	Define the binary product of categories, which has objects for each pair of objects of the factors, and morphisms for each pair of morphisms of the factors. Composition is componentwise. (Contributed by Mario Carneiro, 10-Jan-2017.)
|- X.c = ( r e. _V , s e. _V |-> [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ [_ ( u e. b , v e. b |-> ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. (comp ` ndx ) , ( x e. ( b X. b ) , y e. b |-> ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. (comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. (comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } )
Definition	df-1stf 16000*	Define the first projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- 1stF = ( r e. Cat , s e. Cat |-> [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r X.c s ) ) y ) ) ) >. )