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 39101

Description: Obsolete defintion, use df-rim 20730 instead. Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.) (New usage is discouraged.)

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

Distinct variable group: 𝑠,𝑟,𝑓

**Detailed syntax breakdown of Definition df-rngoiso**
Step	Hyp	Ref	Expression
1		crngoiso 39086	. 2 class RingOpsIso
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crngo 39019	. . 3 class RingOps
5	2	cv 1569	. . . . . . 7 class 𝑟
6		c1st 8020	. . . . . . 7 class 1^st
7	5, 6	cfv 6555	. . . . . 6 class (1^st ‘𝑟)
8	7	crn 5656	. . . . 5 class ran (1^st ‘𝑟)
9	3	cv 1569	. . . . . . 7 class 𝑠
10	9, 6	cfv 6555	. . . . . 6 class (1^st ‘𝑠)
11	10	crn 5656	. . . . 5 class ran (1^st ‘𝑠)
12		vf	. . . . . 6 setvar 𝑓
13	12	cv 1569	. . . . 5 class 𝑓
14	8, 11, 13	wf1o 6554	. . . 4 wff 𝑓:ran (1^st ‘𝑟)⟶1-1ontoran (1^st ‘𝑠)
15		crngohom 39085	. . . . 5 class RingOpsHom
16	5, 9, 15	co 7440	. . . 4 class (𝑟 RingOpsHom 𝑠)
17	14, 12, 16	crab 3416	. . 3 class {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1^st ‘𝑟)⟶1-1ontoran (1^st ‘𝑠)}
18	2, 3, 4, 4, 17	cmpo 7442	. 2 class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1^st ‘𝑟)⟶1-1ontoran (1^st ‘𝑠)})
19	1, 18	wceq 1570	1 wff RingOpsIso = (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RingOpsHom 𝑠) ∣ 𝑓:ran (1^st ‘𝑟)⟶1-1ontoran (1^st ‘𝑠)})

Colors of variables: wff setvar class

This definition is used by: rngoisoval 39102

W3C validator