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 = ( 𝑟 ∈ RingOps , 𝑠 ∈ 𝒫 ran ( 1^st ‘ 𝑟 ) ↦ ∩ { 𝑗 ∈ ( Idl ‘ 𝑟 ) ∣ 𝑠 ⊆ 𝑗 } )

Step	Hyp	Ref	Expression
0		cigen	⊢ IdlGen
1		vr	⊢ 𝑟
2		crngo	⊢ RingOps
3		vs	⊢ 𝑠
4		c1st	⊢ 1^st
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( 1^st ‘ 𝑟 )
7	6	crn	⊢ ran ( 1^st ‘ 𝑟 )
8	7	cpw	⊢ 𝒫 ran ( 1^st ‘ 𝑟 )
9		vj	⊢ 𝑗
10		cidl	⊢ Idl
11	5 10	cfv	⊢ ( Idl ‘ 𝑟 )
12	3	cv	⊢ 𝑠
13	9	cv	⊢ 𝑗
14	12 13	wss	⊢ 𝑠 ⊆ 𝑗
15	14 9 11	crab	⊢ { 𝑗 ∈ ( Idl ‘ 𝑟 ) ∣ 𝑠 ⊆ 𝑗 }
16	15	cint	⊢ ∩ { 𝑗 ∈ ( Idl ‘ 𝑟 ) ∣ 𝑠 ⊆ 𝑗 }
17	1 3 2 8 16	cmpo	⊢ ( 𝑟 ∈ RingOps , 𝑠 ∈ 𝒫 ran ( 1^st ‘ 𝑟 ) ↦ ∩ { 𝑗 ∈ ( Idl ‘ 𝑟 ) ∣ 𝑠 ⊆ 𝑗 } )
18	0 17	wceq	⊢ IdlGen = ( 𝑟 ∈ RingOps , 𝑠 ∈ 𝒫 ran ( 1^st ‘ 𝑟 ) ↦ ∩ { 𝑗 ∈ ( Idl ‘ 𝑟 ) ∣ 𝑠 ⊆ 𝑗 } )

Metamath Proof Explorer