Metamath Proof Explorer

Theorem igenmin

Description: Obsolete theorem, use rspssp instead. The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	igenmin	$⊢ (R \in RingOps \land I \in Idl (R) \land S \subseteq I) \to R IdlGen S \subseteq I$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
2		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
3	1 2	idlss	$⊢ (R \in RingOps \land I \in Idl (R)) \to I \subseteq ran 1^{st} (R)$
4		sstr	$⊢ (S \subseteq I \land I \subseteq ran 1^{st} (R)) \to S \subseteq ran 1^{st} (R)$
5	4	ancoms	$⊢ (I \subseteq ran 1^{st} (R) \land S \subseteq I) \to S \subseteq ran 1^{st} (R)$
6	1 2	igenval	$⊢ (R \in RingOps \land S \subseteq ran 1^{st} (R)) \to R IdlGen S = ⋂ \{j \in Idl (R) \| S \subseteq j\}$
7	5 6	sylan2	$⊢ (R \in RingOps \land (I \subseteq ran 1^{st} (R) \land S \subseteq I)) \to R IdlGen S = ⋂ \{j \in Idl (R) \| S \subseteq j\}$
8	7	anassrs	$⊢ ((R \in RingOps \land I \subseteq ran 1^{st} (R)) \land S \subseteq I) \to R IdlGen S = ⋂ \{j \in Idl (R) \| S \subseteq j\}$
9	3 8	syldanl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land S \subseteq I) \to R IdlGen S = ⋂ \{j \in Idl (R) \| S \subseteq j\}$
10	9	3impa	$⊢ (R \in RingOps \land I \in Idl (R) \land S \subseteq I) \to R IdlGen S = ⋂ \{j \in Idl (R) \| S \subseteq j\}$
11		sseq2	$⊢ j = I \to (S \subseteq j \leftrightarrow S \subseteq I)$
12	11	intminss	$⊢ (I \in Idl (R) \land S \subseteq I) \to ⋂ \{j \in Idl (R) \| S \subseteq j\} \subseteq I$
13	12	3adant1	$⊢ (R \in RingOps \land I \in Idl (R) \land S \subseteq I) \to ⋂ \{j \in Idl (R) \| S \subseteq j\} \subseteq I$
14	10 13	eqsstrd	$⊢ (R \in RingOps \land I \in Idl (R) \land S \subseteq I) \to R IdlGen S \subseteq I$