Definition 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	$$⊢\mathrm{IdlGen}=\left(r\in \mathrm{RingOps},s\in 𝒫\mathrm{ran}{1}^{st}\left(r\right)⟼\bigcap \left\{j\in \mathrm{Idl}\left(r\right)|s\subseteq j\right\}\right)$$

Detailed syntax breakdown

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