P. 404 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40301-40400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rhmsubcrngclem1 40301	Lemma 1 for rhmsubcrngc 40303. (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 40302*	Lemma 2 for rhmsubcrngc 40303. (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 40303	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 40304	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 40305	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 40306	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 40307	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 40308	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 40309*	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 40310*	Lemma 1 for funcringcsetcALTV2 40319. (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 40311*	Lemma 2 for funcringcsetcALTV2 40319. (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 40312*	Lemma 3 for funcringcsetcALTV2 40319. (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 40313*	Lemma 4 for funcringcsetcALTV2 40319. (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 40314*	Lemma 5 for funcringcsetcALTV2 40319. (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 40315*	Lemma 6 for funcringcsetcALTV2 40319. (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 40316*	Lemma 7 for funcringcsetcALTV2 40319. (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 40317*	Lemma 8 for funcringcsetcALTV2 40319. (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 40318*	Lemma 9 for funcringcsetcALTV2 40319. (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 40319*	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 40320	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 40321*	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 40322	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 40323	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 40324*	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 40325	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 40326*	Lemma for ringccatALTV 40327. (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 40327	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 40328	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 40329	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 40330	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 40331	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 40332	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 40333*	Lemma 1 for funcringcsetcALTV 40342. (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 40334*	Lemma 2 for funcringcsetcALTV 40342. (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 40335*	Lemma 3 for funcringcsetcALTV 40342. (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 40336*	Lemma 4 for funcringcsetcALTV 40342. (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 40337*	Lemma 5 for funcringcsetcALTV 40342. (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 40338*	Lemma 6 for funcringcsetcALTV 40342. (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 40339*	Lemma 7 for funcringcsetcALTV 40342. (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 40340*	Lemma 8 for funcringcsetcALTV 40342. (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 40341*	Lemma 9 for funcringcsetcALTV 40342. (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 40342*	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 40343	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 40344	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 40345*	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 40346	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 40347*	Lemma 1 for srhmsubc 40350. (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 40348*	Lemma 2 for srhmsubc 40350. (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 40349*	Lemma 3 for srhmsubc 40350. (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 40350*	According to df-subc 15765, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15793 and subcss2 15796). 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 40351*	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 40352*	According to df-subc 15765, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15793 and subcss2 15796). 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 40353*	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 )
Theorem	drhmsubc 40354*	According to df-subc 15765, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15793 and subcss2 15796). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCat ` U ) ) )
Theorem	drngcat 40355*	The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat J ) e. Cat )
Theorem	fldcat 40356*	The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCat ` U ) |`cat F ) e. Cat )
Theorem	fldc 40357*	The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( ( (RingCat ` U ) |`cat J ) |`cat F ) e. Cat )
Theorem	fldhmsubc 40358*	According to df-subc 15765, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15793 and subcss2 15796). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> F e. (Subcat ` ( (RingCat ` U ) |`cat J ) ) )
Theorem	rngcrescrhm 40359	The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> ( C |`cat H ) = ( ( C ↾s R ) sSet <. ( Hom ` ndx ) , H >. ) )
Theorem	rhmsubclem1 40360	Lemma 1 for rhmsubc 40364. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> H Fn ( R X. R ) )
Theorem	rhmsubclem2 40361	Lemma 2 for rhmsubc 40364. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ph /\ X e. R /\ Y e. R ) -> ( X H Y ) = ( X RingHom Y ) )
Theorem	rhmsubclem3 40362*	Lemma 3 for rhmsubc 40364. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ph /\ x e. R ) -> ( ( Id ` (RngCat ` U ) ) ` x ) e. ( x H x ) )
Theorem	rhmsubclem4 40363*	Lemma 4 for rhmsubc 40364. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. (comp ` (RngCat ` U ) ) z ) f ) e. ( x H z ) )
Theorem	rhmsubc 40364	According to df-subc 15765, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15793 and subcss2 15796). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> H e. (Subcat ` (RngCat ` U ) ) )
Theorem	rhmsubccat 40365	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.)
|- ( ph -> U e. V )   &    |- C = (RngCat ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> ( (RngCat ` U ) |`cat H ) e. Cat )
Theorem	srhmsubcALTVlem1 40366*	Lemma 1 for srhmsubcALTV 40369. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( X e. C -> X e. ( U i^i Ring ) )
Theorem	srhmsubcALTVlem2 40367*	Lemma 2 for srhmsubcALTV 40369. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- A. r e. S r e. Ring   &    |- C = ( U i^i S )   =>    |- ( ( U e. V /\ X e. C ) -> X e. ( Base ` (RingCatALTV ` U ) ) )
Theorem	srhmsubcALTVlem3 40368*	Lemma 3 for srhmsubcALTV 40369. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- 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 ` (RingCatALTV ` U ) ) Y ) )
Theorem	srhmsubcALTV 40369*	According to df-subc 15765, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15793 and subcss2 15796). 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.) (New usage is discouraged.)
|- 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 ` (RingCatALTV ` U ) ) )
Theorem	sringcatALTV 40370*	The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020.) (New usage is discouraged.)
|- 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 -> ( (RingCatALTV ` U ) |`cat J ) e. Cat )
Theorem	crhmsubcALTV 40371*	According to df-subc 15765, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15793 and subcss2 15796). 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.) (New usage is discouraged.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCatALTV ` U ) ) )
Theorem	cringcatALTV 40372*	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.) (New usage is discouraged.)
|- C = ( U i^i CRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat J ) e. Cat )
Theorem	drhmsubcALTV 40373*	According to df-subc 15765, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15793 and subcss2 15796). Therefore, the set of division ring homomorphisms is a "subcategory" of the category of (unital) rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> J e. (Subcat ` (RingCatALTV ` U ) ) )
Theorem	drngcatALTV 40374*	The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat J ) e. Cat )
Theorem	fldcatALTV 40375*	The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( (RingCatALTV ` U ) |`cat F ) e. Cat )
Theorem	fldcALTV 40376*	The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> ( ( (RingCatALTV ` U ) |`cat J ) |`cat F ) e. Cat )
Theorem	fldhmsubcALTV 40377*	According to df-subc 15765, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15793 and subcss2 15796). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020.) (New usage is discouraged.)
|- C = ( U i^i DivRing )   &    |- J = ( r e. C , s e. C |-> ( r RingHom s ) )   &    |- D = ( U i^i Field )   &    |- F = ( r e. D , s e. D |-> ( r RingHom s ) )   =>    |- ( U e. V -> F e. (Subcat ` ( (RingCatALTV ` U ) |`cat J ) ) )
Theorem	rngcrescrhmALTV 40378	The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> ( C |`cat H ) = ( ( C ↾s R ) sSet <. ( Hom ` ndx ) , H >. ) )
Theorem	rhmsubcALTVlem1 40379	Lemma 1 for rhmsubcALTV 40383. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> H Fn ( R X. R ) )
Theorem	rhmsubcALTVlem2 40380	Lemma 2 for rhmsubcALTV 40383. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ph /\ X e. R /\ Y e. R ) -> ( X H Y ) = ( X RingHom Y ) )
Theorem	rhmsubcALTVlem3 40381*	Lemma 3 for rhmsubcALTV 40383. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ph /\ x e. R ) -> ( ( Id ` (RngCatALTV ` U ) ) ` x ) e. ( x H x ) )
Theorem	rhmsubcALTVlem4 40382*	Lemma 4 for rhmsubcALTV 40383. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. (comp ` (RngCatALTV ` U ) ) z ) f ) e. ( x H z ) )
Theorem	rhmsubcALTV 40383	According to df-subc 15765, the subcategories (Subcat ` C ) of a category C are subsets of the homomorphisms of C ( see subcssc 15793 and subcss2 15796). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> H e. (Subcat ` (RngCatALTV ` U ) ) )
Theorem	rhmsubcALTVcat 40384	The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020.) (New usage is discouraged.)
|- ( ph -> U e. V )   &    |- C = (RngCatALTV ` U )   &    |- ( ph -> R = ( Ring i^i U ) )   &    |- H = ( RingHom |` ( R X. R ) )   =>    |- ( ph -> ( (RngCatALTV ` U ) |`cat H ) e. Cat )
21.33.14  Basic algebraic structures (extension)
21.33.14.1  Auxiliary theorems
Theorem	xpprsng 40385	The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019.)
|- ( ( A e. V /\ B e. W /\ C e. U ) -> ( { A , B } X. { C } ) = { <. A , C >. , <. B , C >. } )
Theorem	opeliun2xp 40386	Membership of an ordered pair in a union of Cartesian products over its second component, analogous to opeliunxp 4904. (Contributed by AV, 30-Mar-2019.)
|- ( <. C , y >. e. U_ y e. B ( A X. { y } ) <-> ( y e. B /\ C e. A ) )
Theorem	eliunxp2 40387*	Membership in a union of Cartesian products over its second component, analogous to eliunxp 4990. (Contributed by AV, 30-Mar-2019.)
|- ( C e. U_ y e. B ( A X. { y } ) <-> E. x E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
Theorem	mpt2mptx2 40388*	Express a two-argument function as a one-argument function, or vice-versa. In this version A ( y ) is not assumed to be constant w.r.t y, analogous to mpt2mptx 6413. (Contributed by AV, 30-Mar-2019.)
|- ( z = <. x , y >. -> C = D )   =>    |- ( z e. U_ y e. B ( A X. { y } ) |-> C ) = ( x e. A , y e. B |-> D )
Theorem	cbvmpt2x2 40389*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 6396 allows A to be a function of y, analogous to cbvmpt2x 6395. (Contributed by AV, 30-Mar-2019.)
|- F/_ z A   &    |- F/_ y D   &    |- F/_ z C   &    |- F/_ w C   &    |- F/_ x E   &    |- F/_ y E   &    |- ( y = z -> A = D )   &    |- ( ( y = z /\ x = w ) -> C = E )   =>    |- ( x e. A , y e. B |-> C ) = ( w e. D , z e. B |-> E )
Theorem	dmmpt2ssx2 40390*	The domain of a mapping is a subset of its base classes expressed as union of Cartesian products over its second component, analogous to dmmpt2ssx 6884. (Contributed by AV, 30-Mar-2019.)
|- F = ( x e. A , y e. B |-> C )   =>    |- dom F C_ U_ y e. B ( A X. { y } )
Theorem	mpt2exxg2 40391*	Existence of an operation class abstraction (version for dependent domains, i.e. the first base class may depend on the second base class), analogous to mpt2exxg 6893. (Contributed by AV, 30-Mar-2019.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( B e. R /\ A. y e. B A e. S ) -> F e. _V )
Theorem	ovmpt2rdxf 40392*	Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpt2dxf 6448. (Contributed by AV, 30-Mar-2019.)
|- ( ph -> F = ( x e. C , y e. D |-> R ) )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   &    |- ( ( ph /\ y = B ) -> C = L )   &    |- ( ph -> A e. L )   &    |- ( ph -> B e. D )   &    |- ( ph -> S e. X )   &    |- F/ x ph   &    |- F/ y ph   &    |- F/_ y A   &    |- F/_ x B   &    |- F/_ x S   &    |- F/_ y S   =>    |- ( ph -> ( A F B ) = S )
Theorem	ovmpt2rdx 40393*	Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpt2dxf 6448. (Contributed by AV, 30-Mar-2019.)
|- ( ph -> F = ( x e. C , y e. D |-> R ) )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   &    |- ( ( ph /\ y = B ) -> C = L )   &    |- ( ph -> A e. L )   &    |- ( ph -> B e. D )   &    |- ( ph -> S e. X )   =>    |- ( ph -> ( A F B ) = S )
Theorem	ovmpt2x2 40394*	The value of an operation class abstraction. Variant of ovmpt2ga 6452 which does not require D and x to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|- ( ( x = A /\ y = B ) -> R = S )   &    |- ( y = B -> C = L )   &    |- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. L /\ B e. D /\ S e. H ) -> ( A F B ) = S )
Theorem	fdmdifeqresdif 40395*	The restriction of a conditional mapping to function values of a function having a domain which is a difference with a singleton equals this function. (Contributed by AV, 23-Apr-2019.)
|- F = ( x e. D |-> if ( x = Y , X , ( G ` x ) ) )   =>    |- ( G : ( D \ { Y } ) --> R -> G = ( F |` ( D \ { Y } ) ) )
Theorem	offvalfv 40396*	The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019.)
|- ( ph -> A e. V )   &    |- ( ph -> F Fn A )   &    |- ( ph -> G Fn A )   =>    |- ( ph -> ( F oF R G ) = ( x e. A |-> ( ( F ` x ) R ( G ` x ) ) ) )
Theorem	ofaddmndmap 40397	The function operation applied to the addition for functions (with the same domain) into a monoid is a function (with the same domain) into the monoid. (Contributed by AV, 6-Apr-2019.)
|- R = ( Base ` M )   &    |- .+ = ( +g ` M )   =>    |- ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A oF .+ B ) e. ( R ^m V ) )
Theorem	mapsnop 40398	A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019.)
|- F = { <. X , Y >. }   =>    |- ( ( X e. V /\ Y e. R /\ R e. W ) -> F e. ( R ^m { X } ) )
Theorem	mapprop 40399	An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019.)
|- F = { <. X , A >. , <. Y , B >. }   =>    |- ( ( ( X e. V /\ A e. R ) /\ ( Y e. V /\ B e. R ) /\ ( X =/= Y /\ R e. W ) ) -> F e. ( R ^m { X , Y } ) )
Theorem	ztprmneprm 40400	A prime is not an integer multiple of another prime. (Contributed by AV, 23-May-2019.)
|- ( ( Z e. ZZ /\ A e. Prime /\ B e. Prime ) -> ( ( Z x. A ) = B -> A = B ) )