Metamath Proof Explorer

Theorem igenidl

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

		Ref	Expression
	Hypotheses	igenval.1	$⊢ G = 1^{st} (R)$
		igenval.2	$⊢ X = ran G$
	Assertion	igenidl	$⊢ (R \in RingOps \land S \subseteq X) \to R IdlGen S \in Idl (R)$

Proof

Step	Hyp	Ref	Expression
1		igenval.1	$⊢ G = 1^{st} (R)$
2		igenval.2	$⊢ X = ran G$
3	1 2	igenval	$⊢ (R \in RingOps \land S \subseteq X) \to R IdlGen S = ⋂ \{j \in Idl (R) \| S \subseteq j\}$
4	1 2	rngoidl	$⊢ R \in RingOps \to X \in Idl (R)$
5		sseq2	$⊢ j = X \to (S \subseteq j \leftrightarrow S \subseteq X)$
6	5	rspcev	$⊢ (X \in Idl (R) \land S \subseteq X) \to \exists j \in Idl (R) S \subseteq j$
7	4 6	sylan	$⊢ (R \in RingOps \land S \subseteq X) \to \exists j \in Idl (R) S \subseteq j$
8		rabn0	$⊢ \{j \in Idl (R) \| S \subseteq j\} \neq \emptyset \leftrightarrow \exists j \in Idl (R) S \subseteq j$
9	7 8	sylibr	$⊢ (R \in RingOps \land S \subseteq X) \to \{j \in Idl (R) \| S \subseteq j\} \neq \emptyset$
10		ssrab2	$⊢ \{j \in Idl (R) \| S \subseteq j\} \subseteq Idl (R)$
11		intidl	$⊢ (R \in RingOps \land \{j \in Idl (R) \| S \subseteq j\} \neq \emptyset \land \{j \in Idl (R) \| S \subseteq j\} \subseteq Idl (R)) \to ⋂ \{j \in Idl (R) \| S \subseteq j\} \in Idl (R)$
12	10 11	mp3an3	$⊢ (R \in RingOps \land \{j \in Idl (R) \| S \subseteq j\} \neq \emptyset) \to ⋂ \{j \in Idl (R) \| S \subseteq j\} \in Idl (R)$
13	9 12	syldan	$⊢ (R \in RingOps \land S \subseteq X) \to ⋂ \{j \in Idl (R) \| S \subseteq j\} \in Idl (R)$
14	3 13	eqeltrd	$⊢ (R \in RingOps \land S \subseteq X) \to R IdlGen S \in Idl (R)$