Definition df-igen 35337

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 35336	. 2 class IdlGen
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crngo 35171	. . 3 class RingOps
5	2	cv 1532	. . . . . 6 class 𝑟
6		c1st 7686	. . . . . 6 class 1st
7	5, 6	cfv 6354	. . . . 5 class (1st ‘𝑟)
8	7	crn 5555	. . . 4 class ran (1st ‘𝑟)
9	8	cpw 4538	. . 3 class 𝒫 ran (1st ‘𝑟)
10	3	cv 1532	. . . . . 6 class 𝑠
11		vj	. . . . . . 7 setvar 𝑗
12	11	cv 1532	. . . . . 6 class 𝑗
13	10, 12	wss 3935	. . . . 5 wff 𝑠 ⊆ 𝑗
14		cidl 35284	. . . . . 6 class Idl
15	5, 14	cfv 6354	. . . . 5 class (Idl‘𝑟)
16	13, 11, 15	crab 3142	. . . 4 class {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}
17	16	cint 4875	. . 3 class ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}
18	2, 3, 4, 9, 17	cmpo 7157	. 2 class (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})
19	1, 18	wceq 1533	1 wff IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})

This definition is referenced by:  igenval  35338