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	⊢ ≀ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	ccoss	⊢ ≀ 𝑅
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4		vu	⊢ 𝑢
5	4	cv	⊢ 𝑢
6	2	cv	⊢ 𝑥
7	5 6 0	wbr	⊢ 𝑢 𝑅 𝑥
8	3	cv	⊢ 𝑦
9	5 8 0	wbr	⊢ 𝑢 𝑅 𝑦
10	7 9	wa	⊢ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 )
11	10 4	wex	⊢ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 )
12	11 2 3	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }
13	1 12	wceq	⊢ ≀ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }