Definition df-igen 37231

Description: Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)

Assertion

Ref	Expression
df-igen	⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})

Distinct variable group:   𝑠,𝑟,𝑗

Detailed syntax breakdown of Definition df-igen

Step	Hyp	Ref	Expression
1		cigen 37230	. 2 class IdlGen
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crngo 37065	. . 3 class RingOps
5	2	cv 1538	. . . . . 6 class 𝑟
6		c1st 7975	. . . . . 6 class 1st
7	5, 6	cfv 6542	. . . . 5 class (1st ‘𝑟)
8	7	crn 5676	. . . 4 class ran (1st ‘𝑟)
9	8	cpw 4601	. . 3 class 𝒫 ran (1st ‘𝑟)
10	3	cv 1538	. . . . . 6 class 𝑠
11		vj	. . . . . . 7 setvar 𝑗
12	11	cv 1538	. . . . . 6 class 𝑗
13	10, 12	wss 3947	. . . . 5 wff 𝑠 ⊆ 𝑗
14		cidl 37178	. . . . . 6 class Idl
15	5, 14	cfv 6542	. . . . 5 class (Idl‘𝑟)
16	13, 11, 15	crab 3430	. . . 4 class {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}
17	16	cint 4949	. . 3 class ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}
18	2, 3, 4, 9, 17	cmpo 7413	. 2 class (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})
19	1, 18	wceq 1539	1 wff IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})

This definition is referenced by:  igenval  37232