Definition df-irred

Description: Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Assertion	df-irred	$$⊢\mathrm{Irred}=\left(w\in \mathrm{V}⟼⦋\left({\mathrm{Base}}_w\setminus \mathrm{Unit}\left(w\right)\right)/b⦌\left\{z\in b|\forall x\in b\forall y\in bx{\cdot }_{w}y\ne z\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cir	$$class\mathrm{Irred}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarw$$
5	4 3	cfv	$$class{\mathrm{Base}}_w$$
6		cui	$$class\mathrm{Unit}$$
7	4 6	cfv	$$class\mathrm{Unit}\left(w\right)$$
8	5 7	cdif	$$class\left({\mathrm{Base}}_w\setminus \mathrm{Unit}\left(w\right)\right)$$
9		vb	$$setvarb$$
10		vz	$$setvarz$$
11	9	cv	$$setvarb$$
12		vx	$$setvarx$$
13		vy	$$setvary$$
14	12	cv	$$setvarx$$
15		cmulr	$$class{\cdot }_{𝑟}$$
16	4 15	cfv	$$class{\cdot }_w$$
17	13	cv	$$setvary$$
18	14 17 16	co	$$class\left(x{\cdot }_{w}y\right)$$
19	10	cv	$$setvarz$$
20	18 19	wne	$$wffx{\cdot }_{w}y\ne z$$
21	20 13 11	wral	$$wff\forall y\in bx{\cdot }_{w}y\ne z$$
22	21 12 11	wral	$$wff\forall x\in b\forall y\in bx{\cdot }_{w}y\ne z$$
23	22 10 11	crab	$$class\left\{z\in b|\forall x\in b\forall y\in bx{\cdot }_{w}y\ne z\right\}$$
24	9 8 23	csb	$$class⦋\left({\mathrm{Base}}_w\setminus \mathrm{Unit}\left(w\right)\right)/b⦌\left\{z\in b|\forall x\in b\forall y\in bx{\cdot }_{w}y\ne z\right\}$$
25	1 2 24	cmpt	$$class\left(w\in \mathrm{V}⟼⦋\left({\mathrm{Base}}_w\setminus \mathrm{Unit}\left(w\right)\right)/b⦌\left\{z\in b|\forall x\in b\forall y\in bx{\cdot }_{w}y\ne z\right\}\right)$$
26	0 25	wceq	$$wff\mathrm{Irred}=\left(w\in \mathrm{V}⟼⦋\left({\mathrm{Base}}_w\setminus \mathrm{Unit}\left(w\right)\right)/b⦌\left\{z\in b|\forall x\in b\forall y\in bx{\cdot }_{w}y\ne z\right\}\right)$$