Theorem rnghmfn

Description: The mapping of two non-unital rings to the non-unital ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020)

	Ref	Expression
Assertion	rnghmfn	$$⊢\mathrm{RngHomo}Fn\left(\mathrm{Rng}\times \mathrm{Rng}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-rnghomo	$$⊢\mathrm{RngHomo}=\left(r\in \mathrm{Rng},s\in \mathrm{Rng}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right\}\right)$$
2		ovex	$$⊢w^v\in \mathrm{V}$$
3	2	rabex	$$⊢\left\{f\in \left(w^v\right)|\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right\}\in \mathrm{V}$$
4	3	csbex	$$⊢⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right\}\in \mathrm{V}$$
5	4	csbex	$$⊢⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right\}\in \mathrm{V}$$
6	1 5	fnmpoi	$$⊢\mathrm{RngHomo}Fn\left(\mathrm{Rng}\times \mathrm{Rng}\right)$$