Definition df-igen 33859

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

Assertion

Ref	Expression
df-igen	|- IdlGen = ( r e. RingOps , s e. ~P ran ( 1st ` r ) |-> |^| { j e. ( Idl ` r ) | s C_ j } )

Distinct variable group:   s, r, j

Detailed syntax breakdown of Definition df-igen

Step	Hyp	Ref	Expression
1		cigen 33858	. 2 class IdlGen
2		vr	. . 3 setvar r
3		vs	. . 3 setvar s
4		crngo 33693	. . 3 class RingOps
5	2	cv 1482	. . . . . 6 class r
6		c1st 7166	. . . . . 6 class 1st
7	5, 6	cfv 5888	. . . . 5 class ( 1st ` r )
8	7	crn 5115	. . . 4 class ran ( 1st ` r )
9	8	cpw 4158	. . 3 class ~P ran ( 1st ` r )
10	3	cv 1482	. . . . . 6 class s
11		vj	. . . . . . 7 setvar j
12	11	cv 1482	. . . . . 6 class j
13	10, 12	wss 3574	. . . . 5 wff s C_ j
14		cidl 33806	. . . . . 6 class Idl
15	5, 14	cfv 5888	. . . . 5 class ( Idl ` r )
16	13, 11, 15	crab 2916	. . . 4 class { j e. ( Idl ` r ) | s C_ j }
17	16	cint 4475	. . 3 class |^| { j e. ( Idl ` r ) | s C_ j }
18	2, 3, 4, 9, 17	cmpt2 6652	. 2 class ( r e. RingOps , s e. ~P ran ( 1st ` r ) |-> |^| { j e. ( Idl ` r ) | s C_ j } )
19	1, 18	wceq 1483	1 wff IdlGen = ( r e. RingOps , s e. ~P ran ( 1st ` r ) |-> |^| { j e. ( Idl ` r ) | s C_ j } )

This definition is referenced by:  igenval  33860