Definition df-risc

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

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

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		crngiso	⊢ RngIso
12	3 6 11	co	⊢ ( 𝑟 RngIso 𝑠 )
13	10 12	wcel	⊢ 𝑓 ∈ ( 𝑟 RngIso 𝑠 )
14	13 9	wex	⊢ ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 )
15	8 14	wa	⊢ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) )
16	15 1 2	copab	⊢ { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ) }
17	0 16	wceq	⊢ ≃𝑟 = { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ) }