Theorem risci

Description: Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Assertion	risci	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝑅 ≃𝑟 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		elex2	⊢ ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) → ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) )
2		risc	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 ≃𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) )
3	1 2	syl5ibr	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) → 𝑅 ≃𝑟 𝑆 ) )
4	3	3impia	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ) → 𝑅 ≃𝑟 𝑆 )