Metamath Proof Explorer

Theorem rimrcl

Description: Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019)

Ref Expression
Assertion rimrcl 
|- ( F e. ( R RingIso S ) -> ( R e. _V /\ S e. _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 1 elmpocl 
 |-  ( F e. ( R RingIso S ) -> ( R e. _V /\ S e. _V ) )