Theorem rngimrcl

Description: Reverse closure for an isomorphism of non-unital rings. (Contributed by AV, 22-Feb-2020)

	Ref	Expression
Assertion	rngimrcl	⊢ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) )

Proof

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