Definition df-comembers

Description: Define the class of comember equivalence relations on their domain quotients. (Contributed by Peter Mazsa, 28-Nov-2022) (Revised by Peter Mazsa, 24-Jul-2023)

	Ref	Expression
Assertion	df-comembers	Could not format assertion : No typesetting found for |- CoMembErs = { a | ,~ ( `' _E |` a ) Ers a } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccomembers	Could not format CoMembErs : No typesetting found for class CoMembErs with typecode class
1		va	$$setvara$$
2		cep	$$class\mathrm{E}$$
3	2	ccnv	$$class{\mathrm{E}}^{-1}$$
4	1	cv	$$setvara$$
5	3 4	cres	$$class\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)$$
6	5	ccoss	$$class\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)$$
7		cers	$$class\mathrm{Ers}$$
8	6 4 7	wbr	$$wff\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Ers}a$$
9	8 1	cab	$$class\left\{a|\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Ers}a\right\}$$
10	0 9	wceq	Could not format CoMembErs = { a | ,~ ( `' _E |` a ) Ers a } : No typesetting found for wff CoMembErs = { a | ,~ ( `' _E |` a ) Ers a } with typecode wff