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)

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

Metamath Proof Explorer