Metamath Proof Explorer

Theorem igenidl2

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

		Ref	Expression
	Assertion	igenidl2	$⊢ (R \in RingOps \land I \in Idl (R)) \to R IdlGen I = 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	1 2	igenval	$⊢ (R \in RingOps \land I \subseteq ran 1^{st} (R)) \to R IdlGen I = ⋂ \{j \in Idl (R) \| I \subseteq j\}$
5	3 4	syldan	$⊢ (R \in RingOps \land I \in Idl (R)) \to R IdlGen I = ⋂ \{j \in Idl (R) \| I \subseteq j\}$
6		intmin	$⊢ I \in Idl (R) \to ⋂ \{j \in Idl (R) \| I \subseteq j\} = I$
7	6	adantl	$⊢ (R \in RingOps \land I \in Idl (R)) \to ⋂ \{j \in Idl (R) \| I \subseteq j\} = I$
8	5 7	eqtrd	$⊢ (R \in RingOps \land I \in Idl (R)) \to R IdlGen I = I$