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

Proof

Step Hyp Ref Expression
1 df-rim 
 |-  RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
2 ovex 
 |-  ( r RingHom s ) e. _V
3 2 rabex 
 |-  { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } e. _V
4 1 3 fnmpoi 
 |-  RingIso Fn ( _V X. _V )