Definition df-ers

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 "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 , dfeqvrels2 , dfeqvrels3 and df-eqvrel , dfeqvrel2 , dfeqvrel3 are fully transparent in this regard. However, they lack the domain component ( dom R = A ) of the present df-er . While we acknowledge the need of a domain component, the present df-er 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 R Domain A (i.e. dom R = A see brdomaing ),

but R DomainQss A (i.e. ( dom R /. R ) = A , see brdmqss ), see erim vs. prter3 .

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cers	⊢ Ers
1		cdmqss	⊢ DomainQss
2		ceqvrels	⊢ EqvRels
3	1 2	cres	⊢ ( DomainQss ↾ EqvRels )
4	0 3	wceq	⊢ Ers = ( DomainQss ↾ EqvRels )