Metamath Proof Explorer


Theorem rhmfn

Description: The mapping of two rings to the ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020)

Ref Expression
Assertion rhmfn RingHom Fn ( Ring × Ring )

Proof

Step Hyp Ref Expression
1 dfrhm2 RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) )
2 ovex ( 𝑟 GrpHom 𝑠 ) ∈ V
3 2 inex1 ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) ∈ V
4 1 3 fnmpoi RingHom Fn ( Ring × Ring )