Theorem dmcoels

Description: The domain of coelements in A is the union of A . (Contributed by Rodolfo Medina, 14-Oct-2010) (Revised by Peter Mazsa, 5-Apr-2018) (Revised by Peter Mazsa, 26-Sep-2021)

	Ref	Expression
Assertion	dmcoels	$$⊢\mathrm{dom}\sim A=\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		df-coels	$$⊢\sim A=\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
2	1	dmeqi	$$⊢\mathrm{dom}\sim A=\mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
3		dm1cosscnvepres	$$⊢\mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\bigcup A$$
4	2 3	eqtri	$$⊢\mathrm{dom}\sim A=\bigcup A$$