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 34791
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 𝑢 (cf. dfcoss2 34793 and the comment of dfec2 8029). 𝑅 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 𝑅 (cf. 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 34794) or to the range of a range Cartesian product of classes (cf. dfcoss4 34795), which would make the theorems complicated and confusing. Alternate definition is dfcoss2 34793. Technically, we can define it via composition (dfcoss3 34794) or as the range of a range Cartesian product (dfcoss4 34795), but neither of these definitions reveal directly how the cosets by 𝑅 relate to each other. We define functions ( ~? df-funsALTV , ~? df-funALTV ) and disjoints ( ~? dfdisjs , ~? dfdisjs2 , ~? df-disjALTV , ~? dfdisjALTV2 ) 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 34600 . 2 class 𝑅
3 vu . . . . . . 7 setvar 𝑢
43cv 1600 . . . . . 6 class 𝑢
5 vx . . . . . . 7 setvar 𝑥
65cv 1600 . . . . . 6 class 𝑥
74, 6, 1wbr 4886 . . . . 5 wff 𝑢𝑅𝑥
8 vy . . . . . . 7 setvar 𝑦
98cv 1600 . . . . . 6 class 𝑦
104, 9, 1wbr 4886 . . . . 5 wff 𝑢𝑅𝑦
117, 10wa 386 . . . 4 wff (𝑢𝑅𝑥𝑢𝑅𝑦)
1211, 3wex 1823 . . 3 wff 𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)
1312, 5, 8copab 4948 . 2 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
142, 13wceq 1601 1 wff 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑢𝑅𝑥𝑢𝑅𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  dfcoss2  34793  dfcoss3  34794  dfcoss4  34795  relcoss  34800  cossss  34802  cosseq  34803  1cossres  34806  brcoss  34808  cossssid2  34840  cossid  34852
  Copyright terms: Public domain W3C validator