P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	funcestrcsetc 32501*	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 )
21.25.7.10  The category of non-unital rings The "category of non-unital rings" RngCat is the category of all non-unital rings Rng in a universe and non-unital ring homomorphisms RngHomo between these rings. This category is defined as "category restriction" of the category of extensible structures ExtStrCat, which restricts the objects to non-unital rings and the morphisms to the non-unital ring homomorphisms, while the composition of morphisms is preserved, see df-rngc 32504. Alternatively, the category of non-unital rings could have been defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, see dfrngc2 32517. 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 a subset of the non-unital rings (relativized to a subset or "universe" u) ( u i^i Rng ), see rngcbas 32510, and the morphisms/arrows are the non-unital ring homomorphisms restricted to this subset of the non-unital rings ( RngHomo |` ( B X. B ) ), see rngchomfval 32511, whereas the composition is the ordinary composition of functions, see rngccofval 32515 and rngcco 32516. By showing that the non-unital ring homomorphisms between non-unital rings are a subcategory subset ( C_cat) of the mappings between base sets of extensible structures, see rnghmsscmap 32519, it can be shown that the non-unital ring homomorphisms between non-unital rings are a subcategory (Subcat) of the category of extensible structures, see rnghmsubcsetc 32522. It follows that the category of non-unital rings RngCat is actually a category, see rngccat 32523 with the identity function as identity arrow, see rngcid 32524.
Syntax	crngc 32502	Extend class notation to include the category Rng.
class RngCat
Syntax	crngcOLD 32503	Extend class notation to include the category Rng.
class RngCatOLD
Definition	df-rngc 32504	Definition of the category Rng, relativized to a subset u. This is the category of all non-unital rings in u and homomorphisms between these rings. 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 AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- RngCat = ( u e. _V |-> ( (ExtStrCat ` u ) |`cat ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) )
Definition	df-rngcOLD 32505*	Definition of the category Rng, relativized to a subset u. This is the category of all non-unital rings in u and homomorphisms between these rings. 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. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- RngCatOLD = ( u e. _V |-> [_ ( u i^i Rng ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHomo y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )
Theorem	rngcvalOLD 32506*	Value of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatOLD ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Rng ) )   &    |- ( ph -> H = ( x e. B , y e. B |-> ( x RngHomo y ) ) )   &    |- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	rngcval 32507	Value of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Rng ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ph -> C = ( (ExtStrCat ` U ) |`cat H ) )
Theorem	rnghmresfn 32508	The class of non-unital ring homomorphisms restricted to subsets of non-unital rings is a function. (Contributed by AV, 4-Mar-2020.)
|- ( ph -> B = ( U i^i Rng ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ph -> H Fn ( B X. B ) )
Theorem	rnghmresel 32509	An element of the non-unital ring homomorphisms restricted to a subset of non-unital rings is a non-unital ring homomorphisms. (Contributed by AV, 9-Mar-2020.)
|- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) /\ F e. ( X H Y ) ) -> F e. ( X RngHomo Y ) )
Theorem	rngcbas 32510	Set of objects of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Rng ) )
Theorem	rngchomfval 32511	Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )
Theorem	rngchom 32512	Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X RngHomo Y ) )
Theorem	elrngchom 32513	A morphism of non-unital rings is a function. (Contributed by AV, 27-Feb-2020.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) )
Theorem	rngchomfeqhom 32514	The functionalized Hom-set operation equals the Hom-set operation in the category of non-unital rings (in a universe). (Contributed by AV, 9-Mar-2020.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> ( Hom f ` C ) = ( Hom ` C ) )
Theorem	rngccofval 32515	Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = (comp ` (ExtStrCat ` U ) ) )
Theorem	rngcco 32516	Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- ( ph -> Z e. U )   &    |- ( ph -> F : ( Base ` X ) --> ( Base ` Y ) )   &    |- ( ph -> G : ( Base ` Y ) --> ( Base ` Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )
Theorem	dfrngc2 32517	Alternate definition of the category of non-unital rings (in a universe). (Contributed by AV, 16-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Rng ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   &    |- ( ph -> .x. = (comp ` (ExtStrCat ` U ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	rnghmsscmap2 32518*	The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory subset of the mappings between base sets of non-unital rings (in the same universe). (Contributed by AV, 6-Mar-2020.)
|- ( ph -> U e. V )   &    |- ( ph -> R = (Rng i^i U ) )   =>    |- ( ph -> ( RngHomo |` ( R X. R ) ) C_cat ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
Theorem	rnghmsscmap 32519*	The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory subset of the mappings between base sets of extensible structures (in the same universe). (Contributed by AV, 9-Mar-2020.)
|- ( ph -> U e. V )   &    |- ( ph -> R = (Rng i^i U ) )   =>    |- ( ph -> ( RngHomo |` ( R X. R ) ) C_cat ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
Theorem	rnghmsubcsetclem1 32520	Lemma 1 for rnghmsubcsetc 32522. (Contributed by AV, 9-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = (Rng i^i U ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )
Theorem	rnghmsubcsetclem2 32521*	Lemma 2 for rnghmsubcsetc 32522. (Contributed by AV, 9-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = (Rng i^i U ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. (comp ` C ) z ) f ) e. ( x H z ) )
Theorem	rnghmsubcsetc 32522	The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = (Rng i^i U ) )   &    |- ( ph -> H = ( RngHomo |` ( B X. B ) ) )   =>    |- ( ph -> H e. (Subcat ` C ) )
Theorem	rngccat 32523	The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 9-Mar-2020.)
|- C = (RngCat ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	rngcid 32524	The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (Revised by AV, 10-Mar-2020.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- S = ( Base ` X )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` S ) )
Theorem	rngcsect 32525	A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- E = ( Base ` X )   &    |- S = (Sect ` C )   =>    |- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` E ) ) ) )
Theorem	rngcinv 32526	An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- N = (Inv ` C )   =>    |- ( ph -> ( F ( X N Y ) G <-> ( F e. ( X RngIsom Y ) /\ G = `' F ) ) )
Theorem	rngciso 32527	An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.)
|- C = (RngCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( F e. ( X I Y ) <-> F e. ( X RngIsom Y ) ) )
Theorem	rngcbasOLD 32528	Set of objects of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Rng ) )
Theorem	rngchomfvalOLD 32529*	Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. B , y e. B |-> ( x RngHomo y ) ) )
Theorem	rngchomOLD 32530	Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X RngHomo Y ) )
Theorem	elrngchomOLD 32531	A morphism of non-unital rings is a function. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) )
Theorem	rngccofvalOLD 32532*	Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatOLD ` 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 ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) )
Theorem	rngccoOLD 32533	Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatOLD ` 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 RngHomo Y ) )   &    |- ( ph -> G e. ( Y RngHomo Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )
Theorem	rngccatidOLD 32534*	Lemma for rngccatOLD 32535. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatOLD ` U )   &    |- B = ( Base ` C )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )
Theorem	rngccatOLD 32535	The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatOLD ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	rngcidOLD 32536	The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatOLD ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- S = ( Base ` X )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` S ) )
Theorem	rngcsectOLD 32537	A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- E = ( Base ` X )   &    |- S = (Sect ` C )   =>    |- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RngHomo Y ) /\ G e. ( Y RngHomo X ) /\ ( G o. F ) = ( _I |` E ) ) ) )
Theorem	rngcinvOLD 32538	An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- N = (Inv ` C )   =>    |- ( ph -> ( F ( X N Y ) G <-> ( F e. ( X RngIsom Y ) /\ G = `' F ) ) )
Theorem	rngcisoOLD 32539	An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( F e. ( X I Y ) <-> F e. ( X RngIsom Y ) ) )
Theorem	rngchomffvalOLD 32540*	The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) in maps-to notation for an operation. (Contributed by AV, 1-Mar-2020.) (New usage is discouraged.)
|- C = (RngCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- F = ( Hom f ` C )   =>    |- ( ph -> F = ( x e. B , y e. B |-> ( x RngHomo y ) ) )
Theorem	rngchomrnghmresOLD 32541	The value of the functionalized Hom-set operation in the category of non-unital rings (in a universe) as restriction of the non-unital ring homomorphisms. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- C = (RngCatOLD ` U )   &    |- B = (Rng i^i U )   &    |- ( ph -> U e. V )   &    |- F = ( Hom f ` C )   =>    |- ( ph -> F = ( RngHomo |` ( B X. B ) ) )
Theorem	funcrngcsetc 32542*	The "natural forgetful functor" from the category of non-unital rings into the category of sets which sends each non-unital ring to its underlying set (base set) and the morphisms (non-unital ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 26-Mar-2020.)
|- R = (RngCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RngHomo y ) ) ) )   =>    |- ( ph -> F ( R Func S ) G )
21.25.7.11  The category of (unital) rings The "category of unital rings" RingCat is the category of all (unital) rings Ring in a universe and (unital) ring homomorphisms RingHom between these rings. This category is defined as "category restriction" of the category of extensible structures ExtStrCat, which restricts the objects to (unital) rings and the morphisms to the (unital) ring homomorphisms, while the composition of morphisms is preserved, see df-ringc 32545. Alternatively, the category of unital rings could have been defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, see dfringc2 32558. In the following, we omit the predicate "unital", so that "ring" and "ring homomorphism" (without predicate) always mean "unital ring" and "unital ring homomorphism". 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 a subset of the rings (relativized to a subset or "universe" u) ( u i^i Ring ), see ringcbas 32551, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom |` ( B X. B ) ), see ringchomfval 32552, whereas the composition is the ordinary composition of functions, see ringccofval 32556 and ringcco 32557. By showing that the ring homomorphisms between rings are a subcategory subset ( C_cat) of the mappings between base sets of extensible structures, see rhmsscmap 32560, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 32563. It follows that the category of rings RingCat is actually a category, see ringccat 32564 with the identity function as identity arrow, see ringcid 32565. Furthermore, it is shown that the ring homomorphisms between rings are a subcategory subset of the non-unital ring homomorphisms between non-unital rings, see rhmsscrnghm 32566, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 32569. By this, the restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings, see rngcresringcat 32570: ( (RngCat ` U ) |`cat ( RingHom |` ( B X. B ) ) ) = (RingCat ` U ) ). Finally, it is shown that the "natural forgetful functor" from the category of rings into the category of sets is the function which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets, see funcringcsetc 32575.
Syntax	cringc 32543	Extend class notation to include the category Ring.
class RingCat
Syntax	cringcOLD 32544	Extend class notation to include the category Ring.
class RingCatOLD
Definition	df-ringc 32545	Definition of the category Ring, relativized to a subset u. This is the category of all unital rings in u and homomorphisms between these rings. 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 AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- RingCat = ( u e. _V |-> ( (ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) ) )
Definition	df-ringcOLD 32546*	Definition of the category Ring, relativized to a subset u. This is the category of all rings in u and homomorphisms between these rings. 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 AV, 13-Feb-2020.) (New usage is discouraged.)
|- RingCatOLD = ( u e. _V |-> [_ ( u i^i Ring ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RingHom y ) ) >. , <. (comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RingHom z ) , f e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )
Theorem	ringcvalOLD 32547*	Value of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Ring ) )   &    |- ( ph -> H = ( x e. B , y e. B |-> ( x RingHom y ) ) )   &    |- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RingHom z ) , f e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	ringcval 32548	Value of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RingCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Ring ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ph -> C = ( (ExtStrCat ` U ) |`cat H ) )
Theorem	rhmresfn 32549	The class of unital ring homomorphisms restricted to subsets of unital rings is a function. (Contributed by AV, 10-Mar-2020.)
|- ( ph -> B = ( U i^i Ring ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ph -> H Fn ( B X. B ) )
Theorem	rhmresel 32550	An element of the unital ring homomorphisms restricted to a subset of unital rings is a unital ring homomorphism. (Contributed by AV, 10-Mar-2020.)
|- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) /\ F e. ( X H Y ) ) -> F e. ( X RingHom Y ) )
Theorem	ringcbas 32551	Set of objects of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Ring ) )
Theorem	ringchomfval 32552	Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )
Theorem	ringchom 32553	Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X RingHom Y ) )
Theorem	elringchom 32554	A morphism of unital rings is a function. (Contributed by AV, 14-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) )
Theorem	ringchomfeqhom 32555	The functionalized Hom-set operation equals the Hom-set operation in the category of unital rings (in a universe). (Contributed by AV, 9-Mar-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> ( Hom f ` C ) = ( Hom ` C ) )
Theorem	ringccofval 32556	Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RingCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   =>    |- ( ph -> .x. = (comp ` (ExtStrCat ` U ) ) )
Theorem	ringcco 32557	Composition in the category of unital rings. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 8-Mar-2020.)
|- C = (RingCat ` U )   &    |- ( ph -> U e. V )   &    |- .x. = (comp ` C )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- ( ph -> Z e. U )   &    |- ( ph -> F : ( Base ` X ) --> ( Base ` Y ) )   &    |- ( ph -> G : ( Base ` Y ) --> ( Base ` Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )
Theorem	dfringc2 32558	Alternate definition of the category of unital rings (in a universe). (Contributed by AV, 16-Mar-2020.)
|- C = (RingCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( U i^i Ring ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   &    |- ( ph -> .x. = (comp ` (ExtStrCat ` U ) ) )   =>    |- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .x. >. } )
Theorem	rhmsscmap2 32559*	The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the mappings between base sets of unital rings (in the same universe). (Contributed by AV, 6-Mar-2020.)
|- ( ph -> U e. V )   &    |- ( ph -> R = ( Ring i^i U ) )   =>    |- ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( x e. R , y e. R |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
Theorem	rhmsscmap 32560*	The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the mappings between base sets of extensible structures (in the same universe). (Contributed by AV, 9-Mar-2020.)
|- ( ph -> U e. V )   &    |- ( ph -> R = ( Ring i^i U ) )   =>    |- ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
Theorem	rhmsubcsetclem1 32561	Lemma 1 for rhmsubcsetc 32563. (Contributed by AV, 9-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )
Theorem	rhmsubcsetclem2 32562*	Lemma 2 for rhmsubcsetc 32563. (Contributed by AV, 9-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. (comp ` C ) z ) f ) e. ( x H z ) )
Theorem	rhmsubcsetc 32563	The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of extensible structures. (Contributed by AV, 9-Mar-2020.)
|- C = (ExtStrCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ph -> H e. (Subcat ` C ) )
Theorem	ringccat 32564	The category of unital rings is a category. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 9-Mar-2020.)
|- C = (RingCat ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	ringcid 32565	The identity arrow in the category of unital rings is the identity function. (Contributed by AV, 14-Feb-2020.) (Revised by AV, 10-Mar-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- S = ( Base ` X )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` S ) )
Theorem	rhmsscrnghm 32566	The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the non-unital ring homomorphisms between non-unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.)
|- ( ph -> U e. V )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- ( ph -> S = (Rng i^i U ) )   =>    |- ( ph -> ( RingHom |` ( R X. R ) ) C_cat ( RngHomo |` ( S X. S ) ) )
Theorem	rhmsubcrngclem1 32567	Lemma 1 for rhmsubcrngc 32569. (Contributed by AV, 9-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )
Theorem	rhmsubcrngclem2 32568*	Lemma 2 for rhmsubcrngc 32569. (Contributed by AV, 12-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ( ph /\ x e. B ) -> A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. (comp ` C ) z ) f ) e. ( x H z ) )
Theorem	rhmsubcrngc 32569	The unital ring homomorphisms between unital rings (in a universe) are a subcategory of the category of non-unital rings. (Contributed by AV, 12-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ph -> H e. (Subcat ` C ) )
Theorem	rngcresringcat 32570	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings. (Contributed by AV, 16-Mar-2020.)
|- C = (RngCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> B = ( Ring i^i U ) )   &    |- ( ph -> H = ( RingHom |` ( B X. B ) ) )   =>    |- ( ph -> ( C |`cat H ) = (RingCat ` U ) )
Theorem	ringcsect 32571	A section in the category of unital rings, written out. (Contributed by AV, 14-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- E = ( Base ` X )   &    |- S = (Sect ` C )   =>    |- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) /\ ( G o. F ) = ( _I |` E ) ) ) )
Theorem	ringcinv 32572	An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- N = (Inv ` C )   =>    |- ( ph -> ( F ( X N Y ) G <-> ( F e. ( X RingIso Y ) /\ G = `' F ) ) )
Theorem	ringciso 32573	An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( F e. ( X I Y ) <-> F e. ( X RingIso Y ) ) )
Theorem	ringcbasbas 32574	An element of the base set of the base set of the category of unital rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020.)
|- C = (RingCat ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. WUni )   =>    |- ( ( ph /\ R e. B ) -> ( Base ` R ) e. U )
Theorem	funcringcsetc 32575*	The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 26-Mar-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ph -> F ( R Func S ) G )
Theorem	funcringcsetcOLD2lem1 32576*	Lemma 1 for funcringcsetcOLD2 32585. (Contributed by AV, 15-Feb-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( F ` X ) = ( Base ` X ) )
Theorem	funcringcsetcOLD2lem2 32577*	Lemma 2 for funcringcsetcOLD2 32585. (Contributed by AV, 15-Feb-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( F ` X ) e. U )
Theorem	funcringcsetcOLD2lem3 32578*	Lemma 3 for funcringcsetcOLD2 32585. (Contributed by AV, 15-Feb-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ph -> F : B --> C )
Theorem	funcringcsetcOLD2lem4 32579*	Lemma 4 for funcringcsetcOLD2 32585. (Contributed by AV, 15-Feb-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ph -> G Fn ( B X. B ) )
Theorem	funcringcsetcOLD2lem5 32580*	Lemma 5 for funcringcsetcOLD2 32585. (Contributed by AV, 15-Feb-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) = ( _I |` ( X RingHom Y ) ) )
Theorem	funcringcsetcOLD2lem6 32581*	Lemma 6 for funcringcsetcOLD2 32585. (Contributed by AV, 15-Feb-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) /\ H e. ( X RingHom Y ) ) -> ( ( X G Y ) ` H ) = H )
Theorem	funcringcsetcOLD2lem7 32582*	Lemma 7 for funcringcsetcOLD2 32585. (Contributed by AV, 15-Feb-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( Id ` S ) ` ( F ` X ) ) )
Theorem	funcringcsetcOLD2lem8 32583*	Lemma 8 for funcringcsetcOLD2 32585. (Contributed by AV, 15-Feb-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X G Y ) : ( X ( Hom ` R ) Y ) --> ( ( F ` X ) ( Hom ` S ) ( F ` Y ) ) )
Theorem	funcringcsetcOLD2lem9 32584*	Lemma 9 for funcringcsetcOLD2 32585. (Contributed by AV, 15-Feb-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( H e. ( X ( Hom ` R ) Y ) /\ K e. ( Y ( Hom ` R ) Z ) ) ) -> ( ( X G Z ) ` ( K ( <. X , Y >. (comp ` R ) Z ) H ) ) = ( ( ( Y G Z ) ` K ) ( <. ( F ` X ) , ( F ` Y ) >. (comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` H ) ) )
Theorem	funcringcsetcOLD2 32585*	The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 16-Feb-2020.)
|- R = (RingCat ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )   =>    |- ( ph -> F ( R Func S ) G )
Theorem	ringcbasOLD 32586	Set of objects of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Ring ) )
Theorem	ringchomfvalOLD 32587*	Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. B , y e. B |-> ( x RingHom y ) ) )
Theorem	ringchomOLD 32588	Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X H Y ) = ( X RingHom Y ) )
Theorem	elringchomOLD 32589	A morphism of rings is a function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( F e. ( X H Y ) -> F : ( Base ` X ) --> ( Base ` Y ) ) )
Theorem	ringccofvalOLD 32590*	Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` 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 ) RingHom z ) , f e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) )
Theorem	ringccoOLD 32591	Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` 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 RingHom Y ) )   &    |- ( ph -> G e. ( Y RingHom Z ) )   =>    |- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )
Theorem	ringccatidOLD 32592*	Lemma for ringccatOLD 32593. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- B = ( Base ` C )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )
Theorem	ringccatOLD 32593	The category of rings is a category. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	ringcidOLD 32594	The identity arrow in the category of rings is the identity function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- S = ( Base ` X )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` S ) )
Theorem	ringcsectOLD 32595	A section in the category of rings, written out. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- E = ( Base ` X )   &    |- S = (Sect ` C )   =>    |- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X RingHom Y ) /\ G e. ( Y RingHom X ) /\ ( G o. F ) = ( _I |` E ) ) ) )
Theorem	ringcinvOLD 32596	An inverse in the category of rings is the converse operation. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- N = (Inv ` C )   =>    |- ( ph -> ( F ( X N Y ) G <-> ( F e. ( X RingIso Y ) /\ G = `' F ) ) )
Theorem	ringcisoOLD 32597	An isomorphism in the category of rings is a bijection. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- I = ( Iso ` C )   =>    |- ( ph -> ( F e. ( X I Y ) <-> F e. ( X RingIso Y ) ) )
Theorem	ringcbasbasOLD 32598	An element of the base set of the base set of the category of rings (i.e. the base set of a ring) belongs to the considered weak universe. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatOLD ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. WUni )   =>    |- ( ( ph /\ R e. B ) -> ( Base ` R ) e. U )
Theorem	funcringcsetclem1OLD 32599*	Lemma 1 for funcringcsetcOLD 32608. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatOLD ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( F ` X ) = ( Base ` X ) )
Theorem	funcringcsetclem2OLD 32600*	Lemma 2 for funcringcsetcOLD 32608. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatOLD ` U )   &    |- S = ( SetCat ` U )   &    |- B = ( Base ` R )   &    |- C = ( Base ` S )   &    |- ( ph -> U e. WUni )   &    |- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )   =>    |- ( ( ph /\ X e. B ) -> ( F ` X ) e. U )