P. 384 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38301-38400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngchomfeqhom 38301	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 38302	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 38303	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 38304	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 38305*	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 38306*	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 38307	Lemma 1 for rnghmsubcsetc 38309. (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 38308*	Lemma 2 for rnghmsubcsetc 38309. (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 38309	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 38310	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 38311	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 38312	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 38313	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 38314	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 38315	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 38316*	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 38317	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 38318	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 38319*	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 38320	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 38321*	Lemma for rngccatALTV 38322. (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 38322	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 38323	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 38324	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 38325	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 38326	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 38327*	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 38328	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 38329*	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 38330*	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 38331, using cofuval2 15502 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 38329, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 15744. (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 38331*	Alternate proof of funcrngcsetc 38330, using cofuval2 15502 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 38329, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 15744. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 38330. (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 38332	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 38333	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 38334	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.12.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 38337. 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 38350. 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 38343, and the morphisms/arrows are the ring homomorphisms restricted to this subset of the rings ( RingHom |` ( B X. B ) ), see ringchomfval 38344, whereas the composition is the ordinary composition of functions, see ringccofval 38348 and ringcco 38349. 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 38352, it can be shown that the ring homomorphisms between rings are a subcategory (Subcat) of the category of extensible structures, see rhmsubcsetc 38355. It follows that the category of rings RingCat is actually a category, see ringccat 38356 with the identity function as identity arrow, see ringcid 38357. 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 38358, and that the ring homomorphisms between rings are a subcategory of the category of non-unital rings, see rhmsubcrngc 38361. 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 38362: ( (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 38367.
Syntax	cringc 38335	Extend class notation to include the category Ring.
class RingCat
Syntax	cringcALTV 38336	Extend class notation to include the category Ring. (New usage is discouraged.)
class RingCatALTV
Definition	df-ringc 38337	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 38338*	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 38339*	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 38340	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 38341	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 38342	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 38343	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 38344	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 38345	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 38346	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 38347	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 38348	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 38349	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 38350	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 38351*	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 38352*	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 38353	Lemma 1 for rhmsubcsetc 38355. (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 38354*	Lemma 2 for rhmsubcsetc 38355. (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 38355	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 38356	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 38357	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 38358	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 38359	Lemma 1 for rhmsubcrngc 38361. (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 38360*	Lemma 2 for rhmsubcrngc 38361. (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 38361	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 38362	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 38363	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 38364	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 38365	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 38366	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 38367*	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 38368*	Lemma 1 for funcringcsetcALTV2 38377. (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 38369*	Lemma 2 for funcringcsetcALTV2 38377. (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 38370*	Lemma 3 for funcringcsetcALTV2 38377. (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 38371*	Lemma 4 for funcringcsetcALTV2 38377. (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 38372*	Lemma 5 for funcringcsetcALTV2 38377. (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 38373*	Lemma 6 for funcringcsetcALTV2 38377. (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 38374*	Lemma 7 for funcringcsetcALTV2 38377. (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 38375*	Lemma 8 for funcringcsetcALTV2 38377. (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 38376*	Lemma 9 for funcringcsetcALTV2 38377. (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 38377*	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 38378	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 38379*	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 38380	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 38381	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 38382*	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 38383	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 38384*	Lemma for ringccatALTV 38385. (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 38385	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 38386	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 38387	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 38388	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 38389	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 38390	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 38391*	Lemma 1 for funcringcsetcALTV 38400. (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 38392*	Lemma 2 for funcringcsetcALTV 38400. (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 38393*	Lemma 3 for funcringcsetcALTV 38400. (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 38394*	Lemma 4 for funcringcsetcALTV 38400. (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 38395*	Lemma 5 for funcringcsetcALTV 38400. (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 38396*	Lemma 6 for funcringcsetcALTV 38400. (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 38397*	Lemma 7 for funcringcsetcALTV 38400. (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 38398*	Lemma 8 for funcringcsetcALTV 38400. (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 38399*	Lemma 9 for funcringcsetcALTV 38400. (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 38400*	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 )