Definition df-rngiso 20252

Description: Define the set of ring isomorphisms from 𝑟 to 𝑠. (Contributed by Stefan O'Rear, 7-Mar-2015.)

Assertion

Ref	Expression
df-rngiso	⊢ RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)})

Distinct variable group:   𝑠,𝑟,𝑓

Detailed syntax breakdown of Definition df-rngiso

Step	Hyp	Ref	Expression
1		crs 20249	. 2 class RingIso
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3475	. . 3 class V
5		vf	. . . . . . 7 setvar 𝑓
6	5	cv 1541	. . . . . 6 class 𝑓
7	6	ccnv 5676	. . . . 5 class ◡𝑓
8	3	cv 1541	. . . . . 6 class 𝑠
9	2	cv 1541	. . . . . 6 class 𝑟
10		crh 20248	. . . . . 6 class RingHom
11	8, 9, 10	co 7409	. . . . 5 class (𝑠 RingHom 𝑟)
12	7, 11	wcel 2107	. . . 4 wff ◡𝑓 ∈ (𝑠 RingHom 𝑟)
13	9, 8, 10	co 7409	. . . 4 class (𝑟 RingHom 𝑠)
14	12, 5, 13	crab 3433	. . 3 class {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)}
15	2, 3, 4, 4, 14	cmpo 7411	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)})
16	1, 15	wceq 1542	1 wff RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)})

This definition is referenced by:  isrim0OLD  20259  rimrcl  20260  isrim0  20261  brric  20283