Theorem eldisjn0el

Description: Special case of disjdmqseq (perhaps this is the closest theorem to the former prter2 ). (Contributed by Peter Mazsa, 26-Sep-2021)

	Ref	Expression
Assertion	eldisjn0el	$$⊢ElDisjA\to \left(\neg \varnothing \in A\leftrightarrow \bigcup A/\sim A=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		disjdmqseq	$$⊢Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\to \left(\mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\leftrightarrow \mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)$$
2		df-eldisj	$$⊢ElDisjA\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
3		n0el3	$$⊢\neg \varnothing \in A\leftrightarrow \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A$$
4		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$$
5	4	bicomi	$$⊢\bigcup A/\sim A=A\leftrightarrow \mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A$$
6	3 5	bibi12i	$$⊢\left(\neg \varnothing \in A\leftrightarrow \bigcup A/\sim A=A\right)\leftrightarrow \left(\mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\leftrightarrow \mathrm{dom}\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)/\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\right)$$
7	1 2 6	3imtr4i	$$⊢ElDisjA\to \left(\neg \varnothing \in A\leftrightarrow \bigcup A/\sim A=A\right)$$