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

Definition df-ers 38645
Description: Define the class of equivalence relations on domain quotients (or: domain quotients restricted to equivalence relations).

The present definition of equivalence relation in set.mm df-er 8744 "is not standard", "somewhat cryptic", has no constant 0-ary class and does not follow the traditional transparent reflexive-symmetric-transitive relation way of definition of equivalence. Definitions df-eqvrels 38566, dfeqvrels2 38570, dfeqvrels3 38571 and df-eqvrel 38567, dfeqvrel2 38572, dfeqvrel3 38573 are fully transparent in this regard. However, they lack the domain component (dom 𝑅 = 𝐴) of the present df-er 8744. While we acknowledge the need of a domain component, the present df-er 8744 definition does not utilize the results revealed by the new theorems in the Partition-Equivalence Theorem part below (like pets 38834 and pet 38833). From those theorems follows that the natural domain of equivalence relations is

not 𝑅Domain𝐴 (i.e. dom 𝑅 = 𝐴 see brdomaing 35917),

but 𝑅 DomainQss 𝐴 (i.e. (dom 𝑅 / 𝑅) = 𝐴, see brdmqss 38628), see erimeq 38661 vs. prter3 38864.

While I'm sure we need both equivalence relation df-eqvrels 38566 and equivalence relation on domain quotient df-ers 38645, I'm not sure whether we need a third equivalence relation concept with the present dom 𝑅 = 𝐴 component as well: this needs further investigation. As a default I suppose that these two concepts df-eqvrels 38566 and df-ers 38645 are enough and named the predicate version of the one on domain quotient as the alternate version df-erALTV 38646 of the present df-er 8744. (Contributed by Peter Mazsa, 26-Jun-2021.)

Assertion
Ref Expression
df-ers Ers = ( DomainQss ↾ EqvRels )

Detailed syntax breakdown of Definition df-ers
StepHypRef Expression
1 cers 38187 . 2 class Ers
2 cdmqss 38185 . . 3 class DomainQss
3 ceqvrels 38178 . . 3 class EqvRels
42, 3cres 5691 . 2 class ( DomainQss ↾ EqvRels )
51, 4wceq 1537 1 wff Ers = ( DomainQss ↾ EqvRels )
Colors of variables: wff setvar class
This definition is referenced by:  brers  38649
  Copyright terms: Public domain W3C validator