Metamath Proof Explorer

Theorem isrisc

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

Ref Expression
Hypotheses isrisc.1 ⊢ R ∈ V
isrisc.2 ⊢ S ∈ V
Assertion isrisc ⊢ R ≃ 𝑟 S ↔ R ∈ RingOps ∧ S ∈ RingOps ∧ ∃ f f ∈ R RngIso S

Proof

Step Hyp Ref Expression
1 isrisc.1 ⊢ R ∈ V
2 isrisc.2 ⊢ S ∈ V
3 isriscg ⊢ R ∈ V ∧ S ∈ V → R ≃ 𝑟 S ↔ R ∈ RingOps ∧ S ∈ RingOps ∧ ∃ f f ∈ R RngIso S
4 1 2 3 mp2an ⊢ R ≃ 𝑟 S ↔ R ∈ RingOps ∧ S ∈ RingOps ∧ ∃ f f ∈ R RngIso S