P. 397 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39601-39700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngcsect 39601	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 39602	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 39603	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	rngcbasALTV 39604	Set of objects of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Rng ) )
Theorem	rngchomfvalALTV 39605*	Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. B , y e. B |-> ( x RngHomo y ) ) )
Theorem	rngchomALTV 39606	Set of arrows of the category of non-unital rings (in a universe). (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` 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	elrngchomALTV 39607	A morphism of non-unital rings is a function. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` 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	rngccofvalALTV 39608*	Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` 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	rngccoALTV 39609	Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` 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	rngccatidALTV 39610*	Lemma for rngccatALTV 39611. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020.)
|- C = (RngCatALTV ` U )   &    |- B = ( Base ` C )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )
Theorem	rngccatALTV 39611	The category of non-unital rings is a category. (Contributed by AV, 27-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	rngcidALTV 39612	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 = (RngCatALTV ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- S = ( Base ` X )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` S ) )
Theorem	rngcsectALTV 39613	A section in the category of non-unital rings, written out. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` 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	rngcinvALTV 39614	An inverse in the category of non-unital rings is the converse operation. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` 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	rngcisoALTV 39615	An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020.) (New usage is discouraged.)
|- C = (RngCatALTV ` 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	rngchomffvalALTV 39616*	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 = (RngCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- F = ( Hom f ` C )   =>    |- ( ph -> F = ( x e. B , y e. B |-> ( x RngHomo y ) ) )
Theorem	rngchomrnghmresALTV 39617	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 = (RngCatALTV ` U )   &    |- B = (Rng i^i U )   &    |- ( ph -> U e. V )   &    |- F = ( Hom f ` C )   =>    |- ( ph -> F = ( RngHomo |` ( B X. B ) ) )
Theorem	rngcifuestrc 39618*	The "inclusion functor" from the category of non-unital rings into the category of extensible structures. (Contributed by AV, 30-Mar-2020.)
|- R = (RngCat ` U )   &    |- E = (ExtStrCat ` U )   &    |- B = ( Base ` R )   &    |- ( ph -> U e. V )   &    |- ( ph -> F = ( _I |` B ) )   &    |- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RngHomo y ) ) ) )   =>    |- ( ph -> F ( R Func E ) G )
Theorem	funcrngcsetc 39619*	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. An alternate proof is provided in funcrngcsetcALT 39620, using cofuval2 15791 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc 39618, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 16033. (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 )
Theorem	funcrngcsetcALT 39620*	Alternate proof of funcrngcsetc 39619, using cofuval2 15791 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc 39618, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 16033. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 39619. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- 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 )
Theorem	zrinitorngc 39621	The zero ring is an initial object in the category of nonunital rings. (Contributed by AV, 18-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> Z e. (InitO ` C ) )
Theorem	zrtermorngc 39622	The zero ring is a terminal object in the category of nonunital rings. (Contributed by AV, 17-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> Z e. (TermO ` C ) )
Theorem	zrzeroorngc 39623	The zero ring is a zero object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> Z e. (ZeroO ` C ) )
21.33.13.9  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 39626. 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 39639. 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 39632, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom |` ( B X. B ) ), see ringchomfval 39633, whereas the composition is the ordinary composition of functions, see ringccofval 39637 and ringcco 39638. 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 39641, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 39644. It follows that the category of rings RingCat is actually a category, see ringccat 39645 with the identity function as identity arrow, see ringcid 39646. 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 39647, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 39650. 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 39651: ( (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 39656.
Syntax	cringc 39624	Extend class notation to include the category Ring.
class RingCat
Syntax	cringcALTV 39625	Extend class notation to include the category Ring. (New usage is discouraged.)
class RingCatALTV
Definition	df-ringc 39626	Definition of the category Ring, relativized to a subset u. See also the note in [Lang] p. 91, and the item Rng in [Adamek] p. 478. 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-ringcALTV 39627*	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.)
|- RingCatALTV = ( 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	ringcvalALTV 39628*	Value of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` 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 39629	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 39630	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 39631	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 39632	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 39633	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 39634	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 39635	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 39636	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 39637	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 39638	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 39639	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 39640*	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 39641*	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 39642	Lemma 1 for rhmsubcsetc 39644. (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 39643*	Lemma 2 for rhmsubcsetc 39644. (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 39644	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 39645	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 39646	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 39647	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 39648	Lemma 1 for rhmsubcrngc 39650. (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 39649*	Lemma 2 for rhmsubcrngc 39650. (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 39650	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 39651	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 39652	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 39653	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 39654	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 39655	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 39656*	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	funcringcsetcALTV2lem1 39657*	Lemma 1 for funcringcsetcALTV2 39666. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- 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	funcringcsetcALTV2lem2 39658*	Lemma 2 for funcringcsetcALTV2 39666. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- 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	funcringcsetcALTV2lem3 39659*	Lemma 3 for funcringcsetcALTV2 39666. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- 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	funcringcsetcALTV2lem4 39660*	Lemma 4 for funcringcsetcALTV2 39666. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- 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	funcringcsetcALTV2lem5 39661*	Lemma 5 for funcringcsetcALTV2 39666. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- 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	funcringcsetcALTV2lem6 39662*	Lemma 6 for funcringcsetcALTV2 39666. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- 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	funcringcsetcALTV2lem7 39663*	Lemma 7 for funcringcsetcALTV2 39666. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- 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	funcringcsetcALTV2lem8 39664*	Lemma 8 for funcringcsetcALTV2 39666. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- 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	funcringcsetcALTV2lem9 39665*	Lemma 9 for funcringcsetcALTV2 39666. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- 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	funcringcsetcALTV2 39666*	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.) (New usage is discouraged.)
|- 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	ringcbasALTV 39667	Set of objects of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   =>    |- ( ph -> B = ( U i^i Ring ) )
Theorem	ringchomfvalALTV 39668*	Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. V )   &    |- H = ( Hom ` C )   =>    |- ( ph -> H = ( x e. B , y e. B |-> ( x RingHom y ) ) )
Theorem	ringchomALTV 39669	Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` 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	elringchomALTV 39670	A morphism of rings is a function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` 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	ringccofvalALTV 39671*	Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` 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	ringccoALTV 39672	Composition in the category of rings. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` 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	ringccatidALTV 39673*	Lemma for ringccatALTV 39674. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   =>    |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )
Theorem	ringccatALTV 39674	The category of rings is a category. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   =>    |- ( U e. V -> C e. Cat )
Theorem	ringcidALTV 39675	The identity arrow in the category of rings is the identity function. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- ( ph -> U e. V )   &    |- ( ph -> X e. B )   &    |- S = ( Base ` X )   =>    |- ( ph -> ( .1. ` X ) = ( _I |` S ) )
Theorem	ringcsectALTV 39676	A section in the category of rings, written out. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` 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	ringcinvALTV 39677	An inverse in the category of rings is the converse operation. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` 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	ringcisoALTV 39678	An isomorphism in the category of rings is a bijection. (Contributed by AV, 14-Feb-2020.) (New usage is discouraged.)
|- C = (RingCatALTV ` 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	ringcbasbasALTV 39679	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 = (RingCatALTV ` U )   &    |- B = ( Base ` C )   &    |- ( ph -> U e. WUni )   =>    |- ( ( ph /\ R e. B ) -> ( Base ` R ) e. U )
Theorem	funcringcsetclem1ALTV 39680*	Lemma 1 for funcringcsetcALTV 39689. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` 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	funcringcsetclem2ALTV 39681*	Lemma 2 for funcringcsetcALTV 39689. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` 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	funcringcsetclem3ALTV 39682*	Lemma 3 for funcringcsetcALTV 39689. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` 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	funcringcsetclem4ALTV 39683*	Lemma 4 for funcringcsetcALTV 39689. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` 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	funcringcsetclem5ALTV 39684*	Lemma 5 for funcringcsetcALTV 39689. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` 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	funcringcsetclem6ALTV 39685*	Lemma 6 for funcringcsetcALTV 39689. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` 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	funcringcsetclem7ALTV 39686*	Lemma 7 for funcringcsetcALTV 39689. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` 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	funcringcsetclem8ALTV 39687*	Lemma 8 for funcringcsetcALTV 39689. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` 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	funcringcsetclem9ALTV 39688*	Lemma 9 for funcringcsetcALTV 39689. (Contributed by AV, 15-Feb-2020.) (New usage is discouraged.)
|- R = (RingCatALTV ` 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	funcringcsetcALTV 39689*	The "natural forgetful functor" from the category of 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.) (New usage is discouraged.)
|- R = (RingCatALTV ` 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	irinitoringc 39690	The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of [Adamek] p. 101 , and example in [Lang] p. 58. (Contributed by AV, 3-Apr-2020.)
|- ( ph -> U e. V )   &    |- ( ph -> ℤring e. U )   &    |- C = (RingCat ` U )   =>    |- ( ph -> ℤring e. (InitO ` C ) )
Theorem	zrtermoringc 39691	The zero ring is a terminal object in the category of unital rings. (Contributed by AV, 17-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RingCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> Z e. (TermO ` C ) )
Theorem	zrninitoringc 39692*	The zero ring is not an initial object in the category of unital rings (if the universe contains at least one unital ring different from the zero ring). (Contributed by AV, 18-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RingCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   &    |- ( ph -> E. r e. ( Base ` C ) r e. NzRing )   =>    |- ( ph -> Z e/ (InitO ` C ) )
Theorem	nzerooringczr 39693	There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.)
|- ( ph -> U e. V )   &    |- C = (RingCat ` U )   &    |- ( ph -> Z e. ( Ring \ NzRing ) )   &    |- ( ph -> Z e. U )   &    |- ( ph -> ℤring e. U )   =>    |- ( ph -> (ZeroO ` C ) = (/) )
21.33.13.10  Subcategories of the category of rings
Theorem	srhmsubclem1 39694*	Lemma 1 for srhmsubc 39697. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( X e. C -> X e. ( U i^i Ring ) )
Theorem	srhmsubclem2 39695*	Lemma 2 for srhmsubc 39697. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( ( U e. V /\ X e. C ) -> X e. ( Base ` (RingCat ` U ) ) )
Theorem	srhmsubclem3 39696*	Lemma 3 for srhmsubc 39697. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( ( U e. V /\ ( X e. C /\ Y e. C ) ) -> ( X J Y ) = ( X ( Hom ` (RingCat ` U ) ) Y ) )
Theorem	srhmsubc 39697*	According to df-subc 15716, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15744 and subcss2 15747). Therefore, the set of special ring homomorphisms (i.e. ring homomorphisms from a special ring to another ring of that kind) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCat ` U ) ) )
Theorem	sringcat 39698*	The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat J ) e. Cat )
Theorem	crhmsubc 39699*	According to df-subc 15716, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15744 and subcss2 15747). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCat ` U ) ) )
Theorem	cringcat 39700*	The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative rings". (Contributed by AV, 19-Feb-2020.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat J ) e. Cat )