Theorem dm1cosscnvepres

Description: The domain of cosets of the restricted converse epsilon relation is the union of the restriction. (Contributed by Peter Mazsa, 18-May-2019) (Revised by Peter Mazsa, 26-Sep-2021)

	Ref	Expression
Assertion	dm1cosscnvepres	$$⊢\mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		dmcoss2	$$⊢\mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\mathrm{ran}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
2		rncnvepres	$$⊢\mathrm{ran}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\bigcup A$$
3	1 2	eqtri	$$⊢\mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\bigcup A$$