Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-coss Structured version   Visualization version   GIF version

Definition df-coss 37276
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 37278 and the comment of dfec2 8705). 𝑅 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 37716). Without the definition of 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 37279) or to the range of a range Cartesian product of classes (cf. dfcoss4 37280), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 37278. Technically, we can define it via composition (dfcoss3 37279) or as the range of a range Cartesian product (dfcoss4 37280), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 37546, df-funALTV 37547) and disjoints (dfdisjs 37573, dfdisjs2 37574, df-disjALTV 37570, dfdisjALTV2 37579) with the help of it as well. (Contributed by Peter Mazsa, 9-Jan-2018.)

Assertion
Ref Expression
df-coss 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
Distinct variable group:   𝑢,𝑅,𝑥,𝑦

Detailed syntax breakdown of Definition df-coss
StepHypRef Expression
1 cR . . 3 class 𝑅
21ccoss 37038 . 2 class 𝑅
3 vu . . . . . . 7 setvar 𝑢
43cv 1540 . . . . . 6 class 𝑢
5 vx . . . . . . 7 setvar 𝑥
65cv 1540 . . . . . 6 class 𝑥
74, 6, 1wbr 5148 . . . . 5 wff 𝑢𝑅𝑥
8 vy . . . . . . 7 setvar 𝑦
98cv 1540 . . . . . 6 class 𝑦
104, 9, 1wbr 5148 . . . . 5 wff 𝑢𝑅𝑦
117, 10wa 396 . . . 4 wff (𝑢𝑅𝑥𝑢𝑅𝑦)
1211, 3wex 1781 . . 3 wff 𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)
1312, 5, 8copab 5210 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
142, 13wceq 1541 1 wff 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  dfcoss2  37278  dfcoss3  37279  dfcoss4  37280  cosscnv  37281  coss1cnvres  37282  relcoss  37288  cossss  37290  cosseq  37291  1cossres  37294  brcoss  37296  cossssid2  37333  cossid  37345
  Copyright terms: Public domain W3C validator