Theorem pwdom

Description: Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015)

	Ref	Expression
Assertion	pwdom	$$⊢A\preccurlyeq B\to 𝒫A\preccurlyeq 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		pweq	$$⊢A=\varnothing \to 𝒫A=𝒫\varnothing$$
2	1	breq1d	$$⊢A=\varnothing \to \left(𝒫A\preccurlyeq 𝒫B\leftrightarrow 𝒫\varnothing \preccurlyeq 𝒫B\right)$$
3		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
4	3	brrelex1i	$$⊢A\preccurlyeq B\to A\in \mathrm{V}$$
5		0sdomg	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
6	4 5	syl	$$⊢A\preccurlyeq B\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
7	6	biimpar	$$⊢\left(A\preccurlyeq B\wedge A\ne \varnothing \right)\to \varnothing \prec A$$
8		simpl	$$⊢\left(A\preccurlyeq B\wedge A\ne \varnothing \right)\to A\preccurlyeq B$$
9		fodomr	$$⊢\left(\varnothing \prec A\wedge A\preccurlyeq B\right)\to \exists ff:B\underset{onto}{⟶}A$$
10	7 8 9	syl2anc	$$⊢\left(A\preccurlyeq B\wedge A\ne \varnothing \right)\to \exists ff:B\underset{onto}{⟶}A$$
11		vex	$$⊢f\in \mathrm{V}$$
12		fopwdom	$$⊢\left(f\in \mathrm{V}\wedge f:B\underset{onto}{⟶}A\right)\to 𝒫A\preccurlyeq 𝒫B$$
13	11 12	mpan	$$⊢f:B\underset{onto}{⟶}A\to 𝒫A\preccurlyeq 𝒫B$$
14	13	exlimiv	$$⊢\exists ff:B\underset{onto}{⟶}A\to 𝒫A\preccurlyeq 𝒫B$$
15	10 14	syl	$$⊢\left(A\preccurlyeq B\wedge A\ne \varnothing \right)\to 𝒫A\preccurlyeq 𝒫B$$
16	3	brrelex2i	$$⊢A\preccurlyeq B\to B\in \mathrm{V}$$
17	16	pwexd	$$⊢A\preccurlyeq B\to 𝒫B\in \mathrm{V}$$
18		0ss	$$⊢\varnothing \subseteq B$$
19	18	sspwi	$$⊢𝒫\varnothing \subseteq 𝒫B$$
20		ssdomg	$$⊢𝒫B\in \mathrm{V}\to \left(𝒫\varnothing \subseteq 𝒫B\to 𝒫\varnothing \preccurlyeq 𝒫B\right)$$
21	17 19 20	mpisyl	$$⊢A\preccurlyeq B\to 𝒫\varnothing \preccurlyeq 𝒫B$$
22	2 15 21	pm2.61ne	$$⊢A\preccurlyeq B\to 𝒫A\preccurlyeq 𝒫B$$