df-rngoiso - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-rngoiso		Structured version Visualization version GIF version

Definition df-rngoiso 37371

Description: Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.)

**Assertion**
Ref	Expression
df-rngoiso	⊢ RingOpsIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1^st ‘𝑟)–1-1-onto→ran (1^st ‘𝑠)})

Distinct variable group: 𝑠,𝑟,𝑓

**Detailed syntax breakdown of Definition df-rngoiso**
Step	Hyp	Ref	Expression
1		crngoiso 37356	. 2 class RingOpsIso
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crngo 37289	. . 3 class RingOps
5	2	cv 1533	. . . . . . 7 class 𝑟
6		c1st 7983	. . . . . . 7 class 1^st
7	5, 6	cfv 6542	. . . . . 6 class (1^st ‘𝑟)
8	7	crn 5673	. . . . 5 class ran (1^st ‘𝑟)
9	3	cv 1533	. . . . . . 7 class 𝑠
10	9, 6	cfv 6542	. . . . . 6 class (1^st ‘𝑠)
11	10	crn 5673	. . . . 5 class ran (1^st ‘𝑠)
12		vf	. . . . . 6 setvar 𝑓
13	12	cv 1533	. . . . 5 class 𝑓
14	8, 11, 13	wf1o 6541	. . . 4 wff 𝑓:ran (1^st ‘𝑟)–1-1-onto→ran (1^st ‘𝑠)
15		crngohom 37355	. . . . 5 class RingOpsHom
16	5, 9, 15	co 7414	. . . 4 class (𝑟 RingOpsHom 𝑠)
17	14, 12, 16	crab 3427	. . 3 class {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1^st ‘𝑟)–1-1-onto→ran (1^st ‘𝑠)}
18	2, 3, 4, 4, 17	cmpo 7416	. 2 class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1^st ‘𝑟)–1-1-onto→ran (1^st ‘𝑠)})
19	1, 18	wceq 1534	1 wff RingOpsIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1^st ‘𝑟)–1-1-onto→ran (1^st ‘𝑠)})

Colors of variables: wff setvar class

This definition is referenced by: rngoisoval 37372