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 35764
 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 35766 and the comment of dfec2 8288). 𝑅 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 ). Without the definition of ≀ 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 35767) or to the range of a range Cartesian product of classes (cf. dfcoss4 35768), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 35766. Technically, we can define it via composition (dfcoss3 35767) or as the range of a range Cartesian product (dfcoss4 35768), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 36019, df-funALTV 36020) and disjoints (dfdisjs 36046, dfdisjs2 36047, df-disjALTV 36043, dfdisjALTV2 36052) 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 35558 . 2 class 𝑅
3 vu . . . . . . 7 setvar 𝑢
43cv 1537 . . . . . 6 class 𝑢
5 vx . . . . . . 7 setvar 𝑥
65cv 1537 . . . . . 6 class 𝑥
74, 6, 1wbr 5052 . . . . 5 wff 𝑢𝑅𝑥
8 vy . . . . . . 7 setvar 𝑦
98cv 1537 . . . . . 6 class 𝑦
104, 9, 1wbr 5052 . . . . 5 wff 𝑢𝑅𝑦
117, 10wa 399 . . . 4 wff (𝑢𝑅𝑥𝑢𝑅𝑦)
1211, 3wex 1781 . . 3 wff 𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)
1312, 5, 8copab 5114 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
142, 13wceq 1538 1 wff 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
 Colors of variables: wff setvar class This definition is referenced by:  dfcoss2  35766  dfcoss3  35767  dfcoss4  35768  relcoss  35773  cossss  35775  cosseq  35776  1cossres  35779  brcoss  35781  cossssid2  35813  cossid  35825
 Copyright terms: Public domain W3C validator