Theorem igenidl

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

	Ref	Expression
Hypotheses	igenval.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	igenval.2	⊢ 𝑋 = ran 𝐺
Assertion	igenidl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑅 IdlGen 𝑆 ) ∈ ( Idl ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		igenval.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		igenval.2	⊢ 𝑋 = ran 𝐺
3	1 2	igenval	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )
4	1 2	rngoidl	⊢ ( 𝑅 ∈ RingOps → 𝑋 ∈ ( Idl ‘ 𝑅 ) )
5		sseq2	⊢ ( 𝑗 = 𝑋 → ( 𝑆 ⊆ 𝑗 ↔ 𝑆 ⊆ 𝑋 ) )
6	5	rspcev	⊢ ( ( 𝑋 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝑋 ) → ∃ 𝑗 ∈ ( Idl ‘ 𝑅 ) 𝑆 ⊆ 𝑗 )
7	4 6	sylan	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ∃ 𝑗 ∈ ( Idl ‘ 𝑅 ) 𝑆 ⊆ 𝑗 )
8		rabn0	⊢ ( { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ≠ ∅ ↔ ∃ 𝑗 ∈ ( Idl ‘ 𝑅 ) 𝑆 ⊆ 𝑗 )
9	7 8	sylibr	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ≠ ∅ )
10		ssrab2	⊢ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ⊆ ( Idl ‘ 𝑅 )
11		intidl	⊢ ( ( 𝑅 ∈ RingOps ∧ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ≠ ∅ ∧ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ⊆ ( Idl ‘ 𝑅 ) ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ∈ ( Idl ‘ 𝑅 ) )
12	10 11	mp3an3	⊢ ( ( 𝑅 ∈ RingOps ∧ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ≠ ∅ ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ∈ ( Idl ‘ 𝑅 ) )
13	9 12	syldan	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ∈ ( Idl ‘ 𝑅 ) )
14	3 13	eqeltrd	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑅 IdlGen 𝑆 ) ∈ ( Idl ‘ 𝑅 ) )