Theorem wdompwdom

Description: Weak dominance strengthens to usual dominance on the power sets. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	wdompwdom	$$⊢X{\preccurlyeq }^{*}Y\to 𝒫X\preccurlyeq 𝒫Y$$

Proof

Step	Hyp	Ref	Expression
1		relwdom	$$⊢\mathrm{Rel}{\preccurlyeq }^{*}$$
2	1	brrelex2i	$$⊢X{\preccurlyeq }^{*}Y\to Y\in \mathrm{V}$$
3	2	pwexd	$$⊢X{\preccurlyeq }^{*}Y\to 𝒫Y\in \mathrm{V}$$
4		0ss	$$⊢\varnothing \subseteq Y$$
5	4	sspwi	$$⊢𝒫\varnothing \subseteq 𝒫Y$$
6		ssdomg	$$⊢𝒫Y\in \mathrm{V}\to \left(𝒫\varnothing \subseteq 𝒫Y\to 𝒫\varnothing \preccurlyeq 𝒫Y\right)$$
7	3 5 6	mpisyl	$$⊢X{\preccurlyeq }^{*}Y\to 𝒫\varnothing \preccurlyeq 𝒫Y$$
8		pweq	$$⊢X=\varnothing \to 𝒫X=𝒫\varnothing$$
9	8	breq1d	$$⊢X=\varnothing \to \left(𝒫X\preccurlyeq 𝒫Y\leftrightarrow 𝒫\varnothing \preccurlyeq 𝒫Y\right)$$
10	7 9	imbitrrid	$$⊢X=\varnothing \to \left(X{\preccurlyeq }^{*}Y\to 𝒫X\preccurlyeq 𝒫Y\right)$$
11		brwdomn0	$$⊢X\ne \varnothing \to \left(X{\preccurlyeq }^{*}Y\leftrightarrow \exists zz:Y\underset{onto}{⟶}X\right)$$
12		vex	$$⊢z\in \mathrm{V}$$
13		fopwdom	$$⊢\left(z\in \mathrm{V}\wedge z:Y\underset{onto}{⟶}X\right)\to 𝒫X\preccurlyeq 𝒫Y$$
14	12 13	mpan	$$⊢z:Y\underset{onto}{⟶}X\to 𝒫X\preccurlyeq 𝒫Y$$
15	14	exlimiv	$$⊢\exists zz:Y\underset{onto}{⟶}X\to 𝒫X\preccurlyeq 𝒫Y$$
16	11 15	biimtrdi	$$⊢X\ne \varnothing \to \left(X{\preccurlyeq }^{*}Y\to 𝒫X\preccurlyeq 𝒫Y\right)$$
17	10 16	pm2.61ine	$$⊢X{\preccurlyeq }^{*}Y\to 𝒫X\preccurlyeq 𝒫Y$$