Metamath Proof Explorer

Theorem rngimrcl

Description: Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020)

Ref Expression
Assertion rngimrcl 
|- ( F e. ( R RngIso S ) -> ( R e. _V /\ S e. _V ) )

Proof

Step Hyp Ref Expression
1 df-rngim 
 |-  RngIso = ( r e. _V , s e. _V |-> { f e. ( r RngHom s ) | `' f e. ( s RngHom r ) } )
2 1 elmpocl 
 |-  ( F e. ( R RngIso S ) -> ( R e. _V /\ S e. _V ) )