# Metamath Proof Explorer

## 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}↾}_{\left({B}×{B}\right)}$
Assertion rhmresfn ${⊢}{\phi }\to {H}Fn\left({B}×{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}↾}_{\left({B}×{B}\right)}$
3 rhmfn ${⊢}\mathrm{RingHom}Fn\left(\mathrm{Ring}×\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}×{B}\subseteq \mathrm{Ring}×\mathrm{Ring}$
7 5 5 6 syl2anc ${⊢}{\phi }\to {B}×{B}\subseteq \mathrm{Ring}×\mathrm{Ring}$
8 fnssres ${⊢}\left(\mathrm{RingHom}Fn\left(\mathrm{Ring}×\mathrm{Ring}\right)\wedge {B}×{B}\subseteq \mathrm{Ring}×\mathrm{Ring}\right)\to \left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right)Fn\left({B}×{B}\right)$
9 3 7 8 sylancr ${⊢}{\phi }\to \left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right)Fn\left({B}×{B}\right)$
10 2 fneq1d ${⊢}{\phi }\to \left({H}Fn\left({B}×{B}\right)↔\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right)Fn\left({B}×{B}\right)\right)$
11 9 10 mpbird ${⊢}{\phi }\to {H}Fn\left({B}×{B}\right)$