This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 RingOpsIso 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 RingOpsIso S
4 1 2 3 mp2an ⊢ R ≃ 𝑟 S ↔ R ∈ RingOps ∧ S ∈ RingOps ∧ ∃ f f ∈ R RingOpsIso S