This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑅 ) )