Definition df-coels

Description: Define the class of coelements on the class A , see also the alternate definition dfcoels . Possible definitions are the special cases of dfcoss3 and dfcoss4 . (Contributed by Peter Mazsa, 20-Nov-2019)

	Ref	Expression
Assertion	df-coels	$$⊢\sim A=\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	ccoels	$$class\sim A$$
2		cep	$$class\mathrm{E}$$
3	2	ccnv	$$class{\mathrm{E}}^{-1}$$
4	3 0	cres	$$class\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
5	4	ccoss	$$class\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
6	1 5	wceq	$$wff\sim A=\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$