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

Proof

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