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 \times Ring)$

Step	Hyp	Ref	Expression
1		dfrhm2	$⊢ RingHom = (r \in Ring, s \in Ring ⟼ (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}))$
2		ovex	$⊢ r GrpHom s \in V$
3	2	inex1	$⊢ (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}) \in V$
4	1 3	fnmpoi	$⊢ RingHom Fn (Ring \times Ring)$