df-igen

Description: Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010)

		Ref	Expression
	Assertion	df-igen	$⊢ IdlGen = (r \in RingOps, s \in 𝒫 ran 1^{st} (r) ⟼ ⋂ \{j \in Idl (r) \| s \subseteq j\})$

Step	Hyp	Ref	Expression
0		cigen	$class IdlGen$
1		vr	$setvar r$
2		crngo	$class RingOps$
3		vs	$setvar s$
4		c1st	$class 1^{st}$
5	1	cv	$setvar r$
6	5 4	cfv	$class 1^{st} (r)$
7	6	crn	$class ran 1^{st} (r)$
8	7	cpw	$class 𝒫 ran 1^{st} (r)$
9		vj	$setvar j$
10		cidl	$class Idl$
11	5 10	cfv	$class Idl (r)$
12	3	cv	$setvar s$
13	9	cv	$setvar j$
14	12 13	wss	$wff s \subseteq j$
15	14 9 11	crab	$class \{j \in Idl (r) \| s \subseteq j\}$
16	15	cint	$class ⋂ \{j \in Idl (r) \| s \subseteq j\}$
17	1 3 2 8 16	cmpo	$class (r \in RingOps, s \in 𝒫 ran 1^{st} (r) ⟼ ⋂ \{j \in Idl (r) \| s \subseteq j\})$
18	0 17	wceq	$wff IdlGen = (r \in RingOps, s \in 𝒫 ran 1^{st} (r) ⟼ ⋂ \{j \in Idl (r) \| s \subseteq j\})$

Metamath Proof Explorer