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 X. Ring )

Proof

Step Hyp Ref Expression
1 dfrhm2 
 |-  RingHom = ( r e. Ring , s e. Ring |-> ( ( r GrpHom s ) i^i ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) ) )
2 ovex 
 |-  ( r GrpHom s ) e. _V
3 2 inex1 
 |-  ( ( r GrpHom s ) i^i ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) ) e. _V
4 1 3 fnmpoi 
 |-  RingHom Fn ( Ring X. Ring )