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 38393
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 38395 and the comment of dfec2 8747). 𝑅 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 38833). Without the definition of 𝑅 we should have to relate the right side of these theorems to a composition of a converse (cf. dfcoss3 38396) or to the range of a range Cartesian product of classes (cf. dfcoss4 38397), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 38395. Technically, we can define it via composition (dfcoss3 38396) or as the range of a range Cartesian product (dfcoss4 38397), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions (df-funsALTV 38663, df-funALTV 38664) and disjoints (dfdisjs 38690, dfdisjs2 38691, df-disjALTV 38687, dfdisjALTV2 38696) 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 38162 . 2 class 𝑅
3 vu . . . . . . 7 setvar 𝑢
43cv 1536 . . . . . 6 class 𝑢
5 vx . . . . . . 7 setvar 𝑥
65cv 1536 . . . . . 6 class 𝑥
74, 6, 1wbr 5148 . . . . 5 wff 𝑢𝑅𝑥
8 vy . . . . . . 7 setvar 𝑦
98cv 1536 . . . . . 6 class 𝑦
104, 9, 1wbr 5148 . . . . 5 wff 𝑢𝑅𝑦
117, 10wa 395 . . . 4 wff (𝑢𝑅𝑥𝑢𝑅𝑦)
1211, 3wex 1776 . . 3 wff 𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)
1312, 5, 8copab 5210 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
142, 13wceq 1537 1 wff 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  dfcoss2  38395  dfcoss3  38396  dfcoss4  38397  cosscnv  38398  coss1cnvres  38399  relcoss  38405  cossss  38407  cosseq  38408  1cossres  38411  brcoss  38413  cossssid2  38450  cossid  38462
  Copyright terms: Public domain W3C validator