Definition df-igen 36928

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 36927	. 2 class IdlGen
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		crngo 36762	. . 3 class RingOps
5	2	cv 1541	. . . . . 6 class 𝑟
6		c1st 7973	. . . . . 6 class 1st
7	5, 6	cfv 6544	. . . . 5 class (1st ‘𝑟)
8	7	crn 5678	. . . 4 class ran (1st ‘𝑟)
9	8	cpw 4603	. . 3 class 𝒫 ran (1st ‘𝑟)
10	3	cv 1541	. . . . . 6 class 𝑠
11		vj	. . . . . . 7 setvar 𝑗
12	11	cv 1541	. . . . . 6 class 𝑗
13	10, 12	wss 3949	. . . . 5 wff 𝑠 ⊆ 𝑗
14		cidl 36875	. . . . . 6 class Idl
15	5, 14	cfv 6544	. . . . 5 class (Idl‘𝑟)
16	13, 11, 15	crab 3433	. . . 4 class {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}
17	16	cint 4951	. . 3 class ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}
18	2, 3, 4, 9, 17	cmpo 7411	. 2 class (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})
19	1, 18	wceq 1542	1 wff IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})

This definition is referenced by:  igenval  36929