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 
|- ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ S C_ I ) -> ( R IdlGen S ) C_ I )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
2 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
3 1 2 idlss 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> I C_ ran ( 1st ` R ) )
4 sstr 
 |-  ( ( S C_ I /\ I C_ ran ( 1st ` R ) ) -> S C_ ran ( 1st ` R ) )
5 4 ancoms 
 |-  ( ( I C_ ran ( 1st ` R ) /\ S C_ I ) -> S C_ ran ( 1st ` R ) )
6 1 2 igenval 
 |-  ( ( R e. RingOps /\ S C_ ran ( 1st ` R ) ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
7 5 6 sylan2 
 |-  ( ( R e. RingOps /\ ( I C_ ran ( 1st ` R ) /\ S C_ I ) ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
8 7 anassrs 
 |-  ( ( ( R e. RingOps /\ I C_ ran ( 1st ` R ) ) /\ S C_ I ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
9 3 8 syldanl 
 |-  ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ S C_ I ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
10 9 3impa 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ S C_ I ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
11 sseq2 
 |-  ( j = I -> ( S C_ j <-> S C_ I ) )
12 11 intminss 
 |-  ( ( I e. ( Idl ` R ) /\ S C_ I ) -> |^| { j e. ( Idl ` R ) | S C_ j } C_ I )
13 12 3adant1 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ S C_ I ) -> |^| { j e. ( Idl ` R ) | S C_ j } C_ I )
14 10 13 eqsstrd 
 |-  ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ S C_ I ) -> ( R IdlGen S ) C_ I )