Theorem rimfn

Description: The mapping of two rings to the ring isomorphisms between them is a function. (Contributed by AV, 24-Jul-2025)

	Ref	Expression
Assertion	rimfn	⊢ RingIso Fn ( V × V )

Proof

Step	Hyp	Ref	Expression
1		df-rim	⊢ RingIso = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) } )
2		ovex	⊢ ( 𝑟 RingHom 𝑠 ) ∈ V
3	2	rabex	⊢ { 𝑓 ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) } ∈ V
4	1 3	fnmpoi	⊢ RingIso Fn ( V × V )