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 )