Theorem isrisc

Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	isrisc.1	⊢ 𝑅 ∈ V
	isrisc.2	⊢ 𝑆 ∈ V
Assertion	isrisc	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isrisc.1	⊢ 𝑅 ∈ V
2		isrisc.2	⊢ 𝑆 ∈ V
3		isriscg	⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) ) )
4	1 2 3	mp2an	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) )