Metamath Proof Explorer

Theorem rimrcl2

Description: Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025)

Ref Expression
Assertion rimrcl2 
|- ( F e. ( R RingIso S ) -> S e. Ring )

Proof

Step Hyp Ref Expression
1 rimrhm 
 |-  ( F e. ( R RingIso S ) -> F e. ( R RingHom S ) )
2 rhmrcl2 
 |-  ( F e. ( R RingHom S ) -> S e. Ring )
3 1 2 syl 
 |-  ( F e. ( R RingIso S ) -> S e. Ring )