Metamath Proof Explorer

Theorem rimrcl1

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

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

Proof

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