Definition df-irred 18643

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

Assertion

Ref	Expression
df-irred	|- Irred = ( w e. _V |-> [_ ( ( Base ` w ) \ (Unit ` w ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z } )

Distinct variable group:   w, b, x, y, z

Detailed syntax breakdown of Definition df-irred

Step	Hyp	Ref	Expression
1		cir 18640	. 2 class Irred
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vb	. . . 4 setvar b
5	2	cv 1482	. . . . . 6 class w
6		cbs 15857	. . . . . 6 class Base
7	5, 6	cfv 5888	. . . . 5 class ( Base ` w )
8		cui 18639	. . . . . 6 class Unit
9	5, 8	cfv 5888	. . . . 5 class (Unit ` w )
10	7, 9	cdif 3571	. . . 4 class ( ( Base ` w ) \ (Unit ` w ) )
11		vx	. . . . . . . . . 10 setvar x
12	11	cv 1482	. . . . . . . . 9 class x
13		vy	. . . . . . . . . 10 setvar y
14	13	cv 1482	. . . . . . . . 9 class y
15		cmulr 15942	. . . . . . . . . 10 class .r
16	5, 15	cfv 5888	. . . . . . . . 9 class ( .r ` w )
17	12, 14, 16	co 6650	. . . . . . . 8 class ( x ( .r ` w ) y )
18		vz	. . . . . . . . 9 setvar z
19	18	cv 1482	. . . . . . . 8 class z
20	17, 19	wne 2794	. . . . . . 7 wff ( x ( .r ` w ) y ) =/= z
21	4	cv 1482	. . . . . . 7 class b
22	20, 13, 21	wral 2912	. . . . . 6 wff A. y e. b ( x ( .r ` w ) y ) =/= z
23	22, 11, 21	wral 2912	. . . . 5 wff A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z
24	23, 18, 21	crab 2916	. . . 4 class { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z }
25	4, 10, 24	csb 3533	. . 3 class [_ ( ( Base ` w ) \ (Unit ` w ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z }
26	2, 3, 25	cmpt 4729	. 2 class ( w e. _V |-> [_ ( ( Base ` w ) \ (Unit ` w ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z } )
27	1, 26	wceq 1483	1 wff Irred = ( w e. _V |-> [_ ( ( Base ` w ) \ (Unit ` w ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z } )

This definition is referenced by:  isirred  18699