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 ) |
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 ) |