Theorem rimrcl

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

	Ref	Expression
Assertion	rimrcl	⊢ ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		df-rngiso	⊢ RingIso = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) } )
2	1	elmpocl	⊢ ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) )