Metamath Proof Explorer

Theorem rimrcl

Description: Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019)

Ref Expression
Assertion rimrcl ⊢ F ∈ R RingIso S → R ∈ V ∧ S ∈ V

Proof

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