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 37584
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 37586 and the comment of dfec2 8708). 𝑅 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 38024). Without the definition of 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 37587) or to the range of a range Cartesian product of classes (cf. dfcoss4 37588), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 37586. Technically, we can define it via composition (dfcoss3 37587) or as the range of a range Cartesian product (dfcoss4 37588), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 37854, df-funALTV 37855) and disjoints (dfdisjs 37881, dfdisjs2 37882, df-disjALTV 37878, dfdisjALTV2 37887) 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 37346 . 2 class 𝑅
3 vu . . . . . . 7 setvar 𝑢
43cv 1538 . . . . . 6 class 𝑢
5 vx . . . . . . 7 setvar 𝑥
65cv 1538 . . . . . 6 class 𝑥
74, 6, 1wbr 5147 . . . . 5 wff 𝑢𝑅𝑥
8 vy . . . . . . 7 setvar 𝑦
98cv 1538 . . . . . 6 class 𝑦
104, 9, 1wbr 5147 . . . . 5 wff 𝑢𝑅𝑦
117, 10wa 394 . . . 4 wff (𝑢𝑅𝑥𝑢𝑅𝑦)
1211, 3wex 1779 . . 3 wff 𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)
1312, 5, 8copab 5209 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
142, 13wceq 1539 1 wff 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  dfcoss2  37586  dfcoss3  37587  dfcoss4  37588  cosscnv  37589  coss1cnvres  37590  relcoss  37596  cossss  37598  cosseq  37599  1cossres  37602  brcoss  37604  cossssid2  37641  cossid  37653
  Copyright terms: Public domain W3C validator