rhmresfn

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

Step	Hyp	Ref	Expression
1		rhmresfn.b	$⊢ φ \to B = U \cap Ring$
2		rhmresfn.h	$⊢ φ \to H = {RingHom ↾}_{(B \times B)}$
3		rhmfn	$⊢ RingHom Fn (Ring \times Ring)$
4		inss2	$⊢ U \cap Ring \subseteq Ring$
5	1 4	eqsstrdi	$⊢ φ \to B \subseteq Ring$
6		xpss12	$⊢ (B \subseteq Ring \land B \subseteq Ring) \to B \times B \subseteq Ring \times Ring$
7	5 5 6	syl2anc	$⊢ φ \to B \times B \subseteq Ring \times Ring$
8		fnssres	$⊢ (RingHom Fn (Ring \times Ring) \land B \times B \subseteq Ring \times Ring) \to ({RingHom ↾}_{(B \times B)}) Fn (B \times B)$
9	3 7 8	sylancr	$⊢ φ \to ({RingHom ↾}_{(B \times B)}) Fn (B \times B)$
10	2	fneq1d	$⊢ φ \to (H Fn (B \times B) \leftrightarrow ({RingHom ↾}_{(B \times B)}) Fn (B \times B))$
11	9 10	mpbird	$⊢ φ \to H Fn (B \times B)$

Metamath Proof Explorer