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

Proof

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