This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐻 = ( RngHom ↾ ( 𝐵 × 𝐵 ) ) )
Assertion rnghmresfn ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 rnghmresfn.b ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
2 rnghmresfn.h ⊢ ( 𝜑 → 𝐻 = ( RngHom ↾ ( 𝐵 × 𝐵 ) ) )
3 rnghmfn ⊢ RngHom 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 ⊢ ( ( RngHom Fn ( Rng × Rng ) ∧ ( 𝐵 × 𝐵 ) ⊆ ( Rng × Rng ) ) → ( RngHom ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
9 3 7 8 sylancr ⊢ ( 𝜑 → ( RngHom ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
10 2 fneq1d ⊢ ( 𝜑 → ( 𝐻 Fn ( 𝐵 × 𝐵 ) ↔ ( RngHom ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) ) )
11 9 10 mpbird ⊢ ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )