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=1^{st}\left(R\right)$$
	igenval.2	$$⊢X=\mathrm{ran}G$$
Assertion	igenss	$$⊢\left(R\in \mathrm{RingOps}\wedge S\subseteq X\right)\to S\subseteq R\mathrm{IdlGen}S$$

Proof

Step	Hyp	Ref	Expression
1		igenval.1	$$⊢G=1^{st}\left(R\right)$$
2		igenval.2	$$⊢X=\mathrm{ran}G$$
3		ssintub	$$⊢S\subseteq \bigcap \left\{j\in \mathrm{Idl}\left(R\right)|S\subseteq j\right\}$$
4	1 2	igenval	$$⊢\left(R\in \mathrm{RingOps}\wedge S\subseteq X\right)\to R\mathrm{IdlGen}S=\bigcap \left\{j\in \mathrm{Idl}\left(R\right)|S\subseteq j\right\}$$
5	3 4	sseqtrrid	$$⊢\left(R\in \mathrm{RingOps}\wedge S\subseteq X\right)\to S\subseteq R\mathrm{IdlGen}S$$