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

Metamath Proof Explorer

Definition df-risc

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

Ref Expression
Assertion df-risc ≃𝑟 = { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingOpsIso 𝑠 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crisc ⊢ ≃𝑟
1 vr ⊢ 𝑟
2 vs ⊢ 𝑠
3 1 cv ⊢ 𝑟
4 crngo ⊢ RingOps
5 3 4 wcel ⊢ 𝑟 ∈ RingOps
6 2 cv ⊢ 𝑠
7 6 4 wcel ⊢ 𝑠 ∈ RingOps
8 5 7 wa ⊢ ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps )
9 vf ⊢ 𝑓
10 9 cv ⊢ 𝑓
11 crngoiso ⊢ RingOpsIso
12 3 6 11 co ⊢ ( 𝑟 RingOpsIso 𝑠 )
13 10 12 wcel ⊢ 𝑓 ∈ ( 𝑟 RingOpsIso 𝑠 )
14 13 9 wex ⊢ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingOpsIso 𝑠 )
15 8 14 wa ⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingOpsIso 𝑠 ) )
16 15 1 2 copab ⊢ { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingOpsIso 𝑠 ) ) }
17 0 16 wceq ⊢ ≃𝑟 = { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RingOpsIso 𝑠 ) ) }