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 ∈ R RngIsom S → R ∈ V ∧ S ∈ V

Proof

Step Hyp Ref Expression
1 df-rngisom ⊢ RngIsom = r ∈ V , s ∈ V ⟼ f ∈ r RngHomo s | f -1 ∈ s RngHomo r
2 1 elmpocl ⊢ F ∈ R RngIsom S → R ∈ V ∧ S ∈ V