Theorem dmqs1cosscnvepreseq

Description: Two ways to express the equality of the domain quotient of the coelements on the class A with the class A . (Contributed by Peter Mazsa, 26-Sep-2021)

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

Proof

Step	Hyp	Ref	Expression
1		df-coels	$$⊢\sim A=\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
2	1	dmqseqeq1i	$$⊢\mathrm{dom}\sim A/\sim A=A\leftrightarrow \mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A$$
3		dmqscoelseq	$$⊢\mathrm{dom}\sim A/\sim A=A\leftrightarrow \bigcup A/\sim A=A$$
4	2 3	bitr3i	$$⊢\mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\leftrightarrow \bigcup A/\sim A=A$$