Metamath Proof Explorer

Theorem igenmin

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

		Ref	Expression
	Assertion	igenmin	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ) → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 1^st ‘ 𝑅 ) = ( 1^st ‘ 𝑅 )
2		eqid	⊢ ran ( 1^st ‘ 𝑅 ) = ran ( 1^st ‘ 𝑅 )
3	1 2	idlss	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝐼 ⊆ ran ( 1^st ‘ 𝑅 ) )
4		sstr	⊢ ( ( 𝑆 ⊆ 𝐼 ∧ 𝐼 ⊆ ran ( 1^st ‘ 𝑅 ) ) → 𝑆 ⊆ ran ( 1^st ‘ 𝑅 ) )
5	4	ancoms	⊢ ( ( 𝐼 ⊆ ran ( 1^st ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ) → 𝑆 ⊆ ran ( 1^st ‘ 𝑅 ) )
6	1 2	igenval	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ⊆ ran ( 1^st ‘ 𝑅 ) ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )
7	5 6	sylan2	⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐼 ⊆ ran ( 1^st ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ) ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )
8	7	anassrs	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ⊆ ran ( 1^st ‘ 𝑅 ) ) ∧ 𝑆 ⊆ 𝐼 ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )
9	3 8	syldanl	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑆 ⊆ 𝐼 ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )
10	9	3impa	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ) → ( 𝑅 IdlGen 𝑆 ) = ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } )
11		sseq2	⊢ ( 𝑗 = 𝐼 → ( 𝑆 ⊆ 𝑗 ↔ 𝑆 ⊆ 𝐼 ) )
12	11	intminss	⊢ ( ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ⊆ 𝐼 )
13	12	3adant1	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ) → ∩ { 𝑗 ∈ ( Idl ‘ 𝑅 ) ∣ 𝑆 ⊆ 𝑗 } ⊆ 𝐼 )
14	10 13	eqsstrd	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑆 ⊆ 𝐼 ) → ( 𝑅 IdlGen 𝑆 ) ⊆ 𝐼 )