Theorem igenss

Description: A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	igenval.1	|- G = ( 1st ` R )
	igenval.2	|- X = ran G
Assertion	igenss	|- ( ( R e. RingOps /\ S C_ X ) -> S C_ ( R IdlGen S ) )

Proof

Step	Hyp	Ref	Expression
1		igenval.1	|- G = ( 1st ` R )
2		igenval.2	|- X = ran G
3		ssintub	|- S C_ |^| { j e. ( Idl ` R ) | S C_ j }
4	1 2	igenval	|- ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
5	3 4	sseqtrrid	|- ( ( R e. RingOps /\ S C_ X ) -> S C_ ( R IdlGen S ) )