Theorem rhmresfn

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

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

Proof

Step	Hyp	Ref	Expression
1		rhmresfn.b	$$⊢\phi \to B=U\cap \mathrm{Ring}$$
2		rhmresfn.h	$$⊢\phi \to H={\mathrm{RingHom}\upharpoonright }_{\left(B\times B\right)}$$
3		rhmfn	$$⊢\mathrm{RingHom}Fn\left(\mathrm{Ring}\times \mathrm{Ring}\right)$$
4		inss2	$$⊢U\cap \mathrm{Ring}\subseteq \mathrm{Ring}$$
5	1 4	eqsstrdi	$$⊢\phi \to B\subseteq \mathrm{Ring}$$
6		xpss12	$$⊢\left(B\subseteq \mathrm{Ring}\wedge B\subseteq \mathrm{Ring}\right)\to B\times B\subseteq \mathrm{Ring}\times \mathrm{Ring}$$
7	5 5 6	syl2anc	$$⊢\phi \to B\times B\subseteq \mathrm{Ring}\times \mathrm{Ring}$$
8		fnssres	$$⊢\left(\mathrm{RingHom}Fn\left(\mathrm{Ring}\times \mathrm{Ring}\right)\wedge B\times B\subseteq \mathrm{Ring}\times \mathrm{Ring}\right)\to \left({\mathrm{RingHom}\upharpoonright }_{\left(B\times B\right)}\right)Fn\left(B\times B\right)$$
9	3 7 8	sylancr	$$⊢\phi \to \left({\mathrm{RingHom}\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{RingHom}\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)$$