Theorem rnghmresfn

Description: The class of non-unital ring homomorphisms restricted to subsets of non-unital rings is a function. (Contributed by AV, 4-Mar-2020)

	Ref	Expression
Hypotheses	rnghmresfn.b	$$⊢\phi \to B=U\cap \mathrm{Rng}$$
	rnghmresfn.h	$$⊢\phi \to H={\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}$$
Assertion	rnghmresfn	$$⊢\phi \to HFn\left(B\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rnghmresfn.b	$$⊢\phi \to B=U\cap \mathrm{Rng}$$
2		rnghmresfn.h	$$⊢\phi \to H={\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}$$
3		rnghmfn	$$⊢\mathrm{RngHomo}Fn\left(\mathrm{Rng}\times \mathrm{Rng}\right)$$
4		inss2	$$⊢U\cap \mathrm{Rng}\subseteq \mathrm{Rng}$$
5	1 4	eqsstrdi	$$⊢\phi \to B\subseteq \mathrm{Rng}$$
6		xpss12	$$⊢\left(B\subseteq \mathrm{Rng}\wedge B\subseteq \mathrm{Rng}\right)\to B\times B\subseteq \mathrm{Rng}\times \mathrm{Rng}$$
7	5 5 6	syl2anc	$$⊢\phi \to B\times B\subseteq \mathrm{Rng}\times \mathrm{Rng}$$
8		fnssres	$$⊢\left(\mathrm{RngHomo}Fn\left(\mathrm{Rng}\times \mathrm{Rng}\right)\wedge B\times B\subseteq \mathrm{Rng}\times \mathrm{Rng}\right)\to \left({\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}\right)Fn\left(B\times B\right)$$
9	3 7 8	sylancr	$$⊢\phi \to \left({\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}\right)Fn\left(B\times B\right)$$
10	2	fneq1d	$$⊢\phi \to \left(HFn\left(B\times B\right)\leftrightarrow \left({\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}\right)Fn\left(B\times B\right)\right)$$
11	9 10	mpbird	$$⊢\phi \to HFn\left(B\times B\right)$$