Definition df-igen

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cigen	|- IdlGen
1		vr	|- r
2		crngo	|- RingOps
3		vs	|- s
4		c1st	|- 1st
5	1	cv	|- r
6	5 4	cfv	|- ( 1st ` r )
7	6	crn	|- ran ( 1st ` r )
8	7	cpw	|- ~P ran ( 1st ` r )
9		vj	|- j
10		cidl	|- Idl
11	5 10	cfv	|- ( Idl ` r )
12	3	cv	|- s
13	9	cv	|- j
14	12 13	wss	|- s C_ j
15	14 9 11	crab	|- { j e. ( Idl ` r ) | s C_ j }
16	15	cint	|- |^| { j e. ( Idl ` r ) | s C_ j }
17	1 3 2 8 16	cmpo	|- ( r e. RingOps , s e. ~P ran ( 1st ` r ) |-> |^| { j e. ( Idl ` r ) | s C_ j } )
18	0 17	wceq	|- IdlGen = ( r e. RingOps , s e. ~P ran ( 1st ` r ) |-> |^| { j e. ( Idl ` r ) | s C_ j } )