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 
|- G = ( 1st ` R )
igenval.2 
|- X = ran G
Assertion igenidl 
|- ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) e. ( Idl ` R ) )

Proof

Step Hyp Ref Expression
1 igenval.1 
 |-  G = ( 1st ` R )
2 igenval.2 
 |-  X = ran G
3 1 2 igenval 
 |-  ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
4 1 2 rngoidl 
 |-  ( R e. RingOps -> X e. ( Idl ` R ) )
5 sseq2 
 |-  ( j = X -> ( S C_ j <-> S C_ X ) )
6 5 rspcev 
 |-  ( ( X e. ( Idl ` R ) /\ S C_ X ) -> E. j e. ( Idl ` R ) S C_ j )
7 4 6 sylan 
 |-  ( ( R e. RingOps /\ S C_ X ) -> E. j e. ( Idl ` R ) S C_ j )
8 rabn0 
 |-  ( { j e. ( Idl ` R ) | S C_ j } =/= (/) <-> E. j e. ( Idl ` R ) S C_ j )
9 7 8 sylibr 
 |-  ( ( R e. RingOps /\ S C_ X ) -> { j e. ( Idl ` R ) | S C_ j } =/= (/) )
10 ssrab2 
 |-  { j e. ( Idl ` R ) | S C_ j } C_ ( Idl ` R )
11 intidl 
 |-  ( ( R e. RingOps /\ { j e. ( Idl ` R ) | S C_ j } =/= (/) /\ { j e. ( Idl ` R ) | S C_ j } C_ ( Idl ` R ) ) -> |^| { j e. ( Idl ` R ) | S C_ j } e. ( Idl ` R ) )
12 10 11 mp3an3 
 |-  ( ( R e. RingOps /\ { j e. ( Idl ` R ) | S C_ j } =/= (/) ) -> |^| { j e. ( Idl ` R ) | S C_ j } e. ( Idl ` R ) )
13 9 12 syldan 
 |-  ( ( R e. RingOps /\ S C_ X ) -> |^| { j e. ( Idl ` R ) | S C_ j } e. ( Idl ` R ) )
14 3 13 eqeltrd 
 |-  ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) e. ( Idl ` R ) )