**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 8412 "is not
standard", "somewhat cryptic", has no costant 0-ary class
and does not
follow the traditional transparent reflexive-symmetric-transitive relation
way of definition of equivalence. Definitions df-eqvrels 36464,
dfeqvrels2 36468, dfeqvrels3 36469 and df-eqvrel 36465, dfeqvrel2 36470, dfeqvrel3 36471
are fully transparent in this regard. However, they lack the domain
component (dom 𝑅 = 𝐴) of the present df-er 8412. While we acknowledge
the need of a domain component, the present df-er 8412 definition does not
utilize the results revealed by the new theorems in the
Partition-Equivalence Theorem part below (like ~? pets and ~? pet ).
From those theorems follows that the natural domain of equivalence
relations is
not 𝑅Domain𝐴 (i.e. dom 𝑅 = 𝐴 see brdomaing 34003),
but 𝑅
DomainQss 𝐴 (i.e.
(dom 𝑅
**/** 𝑅) = 𝐴, see brdmqss 36526), see
erim 36557 vs. prter3 36663.
While I'm sure we need both equivalence relation df-eqvrels 36464 and
equivalence relation on domain quotient df-ers 36542, 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 36464 and df-ers 36542 are enough and
named the predicate version of the one on domain quotient as the alternate
version df-erALTV 36543 of the present df-er 8412. (Contributed by Peter Mazsa,
26-Jun-2021.) |