Definition df-igen 33029

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 33028	. 2 class IdlGen
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crngo 32863	. . 3 class RingOps
5	2	cv 1474	. . . . . 6 class 𝑟
6		c1st 7057	. . . . . 6 class 1st
7	5, 6	cfv 5804	. . . . 5 class (1st ‘𝑟)
8	7	crn 5039	. . . 4 class ran (1st ‘𝑟)
9	8	cpw 4108	. . 3 class 𝒫 ran (1st ‘𝑟)
10	3	cv 1474	. . . . . 6 class 𝑠
11		vj	. . . . . . 7 setvar 𝑗
12	11	cv 1474	. . . . . 6 class 𝑗
13	10, 12	wss 3540	. . . . 5 wff 𝑠 ⊆ 𝑗
14		cidl 32976	. . . . . 6 class Idl
15	5, 14	cfv 5804	. . . . 5 class (Idl‘𝑟)
16	13, 11, 15	crab 2900	. . . 4 class {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}
17	16	cint 4410	. . 3 class ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}
18	2, 3, 4, 9, 17	cmpt2 6551	. 2 class (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})
19	1, 18	wceq 1475	1 wff IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})

This definition is referenced by:  igenval  33030