This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rimrcl

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

		Ref	Expression
	Assertion	rimrcl	$⊢ F \in (R RingIso S) \to (R \in V \land S \in V)$

Step	Hyp	Ref	Expression
1		df-rim	$⊢ RingIso = (r \in V, s \in V ⟼ \{f \in (r RingHom s) \| f^{-1} \in (s RingHom r)\})$
2	1	elmpocl	$⊢ F \in (R RingIso S) \to (R \in V \land S \in V)$