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	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
	rnghmresfn.h	⊢ ( 𝜑 → 𝐻 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
Assertion	rnghmresfn	⊢ ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rnghmresfn.b	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
2		rnghmresfn.h	⊢ ( 𝜑 → 𝐻 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
3		rnghmfn	⊢ RngHomo Fn ( Rng × Rng )
4		inss2	⊢ ( 𝑈 ∩ Rng ) ⊆ Rng
5	1 4	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ Rng )
6		xpss12	⊢ ( ( 𝐵 ⊆ Rng ∧ 𝐵 ⊆ Rng ) → ( 𝐵 × 𝐵 ) ⊆ ( Rng × Rng ) )
7	5 5 6	syl2anc	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) ⊆ ( Rng × Rng ) )
8		fnssres	⊢ ( ( RngHomo Fn ( Rng × Rng ) ∧ ( 𝐵 × 𝐵 ) ⊆ ( Rng × Rng ) ) → ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
9	3 7 8	sylancr	⊢ ( 𝜑 → ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
10	2	fneq1d	⊢ ( 𝜑 → ( 𝐻 Fn ( 𝐵 × 𝐵 ) ↔ ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) ) )
11	9 10	mpbird	⊢ ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )