Definition df-coss

Description: Define the class of cosets by R : x and y are cosets by R iff there exists a set u such that both u R x and u R y hold, i.e., both x and y are are elements of the R -coset of u (see dfcoss2 and the comment of dfec2 ). R is usually a relation.

This concept simplifies theorems relating partition and equivalence: the left side of these theorems relate to R , the right side relate to ,R (see e.g. ~? pet ). Without the definition of ,R we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 ) or to the range of a range Cartesian product of classes (cf. dfcoss4 ), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 . Technically, we can define it via composition ( dfcoss3 ) or as the range of a range Cartesian product ( dfcoss4 ), but neither of these definitions reveal directly how the cosets by R relate to each other. We define functions ( df-funsALTV , df-funALTV ) and disjoints ( dfdisjs , dfdisjs2 , df-disjALTV , dfdisjALTV2 ) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018)

	Ref	Expression
Assertion	df-coss	$$⊢\wr R=\left\{⟨x,y⟩|\exists u\left(uRx\wedge uRy\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1	0	ccoss	$$class\wr R$$
2		vx	$$setvarx$$
3		vy	$$setvary$$
4		vu	$$setvaru$$
5	4	cv	$$setvaru$$
6	2	cv	$$setvarx$$
7	5 6 0	wbr	$$wffuRx$$
8	3	cv	$$setvary$$
9	5 8 0	wbr	$$wffuRy$$
10	7 9	wa	$$wff\left(uRx\wedge uRy\right)$$
11	10 4	wex	$$wff\exists u\left(uRx\wedge uRy\right)$$
12	11 2 3	copab	$$class\left\{⟨x,y⟩|\exists u\left(uRx\wedge uRy\right)\right\}$$
13	1 12	wceq	$$wff\wr R=\left\{⟨x,y⟩|\exists u\left(uRx\wedge uRy\right)\right\}$$