Metamath Proof Explorer

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 = r ∈ V , s ∈ V ⟼ f ∈ r RingHom s | f -1 ∈ s RingHom r
2 ovex ⊢ r RingHom s ∈ V
3 2 rabex ⊢ f ∈ r RingHom s | f -1 ∈ s RingHom r ∈ V
4 1 3 fnmpoi ⊢ RingIso Fn V × V