Theorem igenidl2

Description: The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Assertion	igenidl2	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑅 IdlGen 𝐼 ) = 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 1st ‘ 𝑅 ) = ( 1st ‘ 𝑅 )
2		eqid	⊢ ran ( 1st ‘ 𝑅 ) = ran ( 1st ‘ 𝑅 )
3	1 2	idlss	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝐼 ⊆ ran ( 1st ‘ 𝑅 ) )
4	1 2	igenval	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ⊆ ran ( 1st ‘ 𝑅 ) ) → ( 𝑅 IdlGen 𝐼 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } )
5	3 4	syldan	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑅 IdlGen 𝐼 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } )
6		intmin	⊢ ( 𝐼 ∈ ( Idl ‘ 𝑅 ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } = 𝐼 )
7	6	adantl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝐼 ⊆ 𝑗 } = 𝐼 )
8	5 7	eqtrd	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑅 IdlGen 𝐼 ) = 𝐼 )