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	|- ,~ R = { <. x , y >. | E. u ( u R x /\ u R y ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1	0	ccoss	|- ,~ R
2		vx	|- x
3		vy	|- y
4		vu	|- u
5	4	cv	|- u
6	2	cv	|- x
7	5 6 0	wbr	|- u R x
8	3	cv	|- y
9	5 8 0	wbr	|- u R y
10	7 9	wa	|- ( u R x /\ u R y )
11	10 4	wex	|- E. u ( u R x /\ u R y )
12	11 2 3	copab	|- { <. x , y >. | E. u ( u R x /\ u R y ) }
13	1 12	wceq	|- ,~ R = { <. x , y >. | E. u ( u R x /\ u R y ) }