| Description: Define the class of
cosets by 𝑅: 𝑥 and 𝑦 are cosets by
       𝑅 iff there exists a set 𝑢 such
that both 𝑢𝑅𝑥 and
       𝑢𝑅𝑦 hold, i.e., both 𝑥 and
𝑦
are are elements of the 𝑅
       -coset of 𝑢 (see dfcoss2 38415 and the comment of dfec2 8749). 𝑅 is
       usually a relation. 
       This concept simplifies theorems relating partition and equivalence: the
       left side of these theorems relate to 𝑅, the right side relate to
       ≀ 𝑅 (see e.g. pet 38853).
Without the definition of ≀ 𝑅 we
       should have to relate the right side of these theorems to a composition
       of a converse (cf. dfcoss3 38416) or to the range of a range Cartesian
       product of classes (cf. dfcoss4 38417), which would make the theorems
       complicated and confusing.  Alternate definition is dfcoss2 38415.
       Technically, we can define it via composition (dfcoss3 38416) or as the
       range of a range Cartesian product (dfcoss4 38417), but neither of these
       definitions reveal directly how the cosets by 𝑅 relate to each
       other.  We define functions (df-funsALTV 38683, df-funALTV 38684) and
       disjoints (dfdisjs 38710, dfdisjs2 38711, df-disjALTV 38707, dfdisjALTV2 38716)
       with the help of it as well.  (Contributed by Peter Mazsa,
       9-Jan-2018.) |