Definition df-dvdsr 15701

Description: Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through ( ||_r ` (opp<sub>r</sub> ` R ) ). (Contributed by Mario Carneiro, 1-Dec-2014.)

Assertion

Ref	Expression
df-dvdsr	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )

Distinct variable group:   x, w, y, z

Detailed syntax breakdown of Definition df-dvdsr

Step	Hyp	Ref	Expression
1		cdsr 15698	. 2 class ||r
2		vw	. . 3 set w
3		cvv 2916	. . 3 class _V
4		vx	. . . . . . 7 set x
5	4	cv 1648	. . . . . 6 class x
6	2	cv 1648	. . . . . . 7 class w
7		cbs 13424	. . . . . . 7 class Base
8	6, 7	cfv 5413	. . . . . 6 class ( Base ` w )
9	5, 8	wcel 1721	. . . . 5 wff x e. ( Base ` w )
10		vz	. . . . . . . . 9 set z
11	10	cv 1648	. . . . . . . 8 class z
12		cmulr 13485	. . . . . . . . 9 class .r
13	6, 12	cfv 5413	. . . . . . . 8 class ( .r ` w )
14	11, 5, 13	co 6040	. . . . . . 7 class ( z ( .r ` w ) x )
15		vy	. . . . . . . 8 set y
16	15	cv 1648	. . . . . . 7 class y
17	14, 16	wceq 1649	. . . . . 6 wff ( z ( .r ` w ) x ) = y
18	17, 10, 8	wrex 2667	. . . . 5 wff E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y
19	9, 18	wa 359	. . . 4 wff ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y )
20	19, 4, 15	copab 4225	. . 3 class { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) }
21	2, 3, 20	cmpt 4226	. 2 class ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
22	1, 21	wceq 1649	1 wff ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )

This definition is referenced by:  reldvdsr  15704  dvdsrval  15705