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 φ B = U Ring
rhmresfn.h φ H = RingHom B × B
Assertion rhmresfn φ H Fn B × B

Proof

Step Hyp Ref Expression
1 rhmresfn.b φ B = U Ring
2 rhmresfn.h φ H = RingHom B × B
3 rhmfn RingHom Fn Ring × Ring
4 inss2 U Ring Ring
5 1 4 eqsstrdi φ B Ring
6 xpss12 B Ring B Ring B × B Ring × Ring
7 5 5 6 syl2anc φ B × B Ring × Ring
8 fnssres RingHom Fn Ring × Ring B × B Ring × Ring RingHom B × B Fn B × B
9 3 7 8 sylancr φ RingHom B × B Fn B × B
10 2 fneq1d φ H Fn B × B RingHom B × B Fn B × B
11 9 10 mpbird φ H Fn B × B