Theorem sspwimp

Description: If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of TakeutiZaring p. 18. For the biconditional, see sspwb . The proof sspwimp , using conventional notation, was translated from virtual deduction form, sspwimpVD , using a translation program. (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sspwimp	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	a1i	$$⊢\top \to x\in \mathrm{V}$$
3		id	$$⊢A\subseteq B\to A\subseteq B$$
4		id	$$⊢x\in 𝒫A\to x\in 𝒫A$$
5		elpwi	$$⊢x\in 𝒫A\to x\subseteq A$$
6	4 5	syl	$$⊢x\in 𝒫A\to x\subseteq A$$
7		sstr	$$⊢\left(x\subseteq A\wedge A\subseteq B\right)\to x\subseteq B$$
8	7	ancoms	$$⊢\left(A\subseteq B\wedge x\subseteq A\right)\to x\subseteq B$$
9	3 6 8	syl2an	$$⊢\left(A\subseteq B\wedge x\in 𝒫A\right)\to x\subseteq B$$
10	2 9	elpwgded	$$⊢\left(\top \wedge \left(A\subseteq B\wedge x\in 𝒫A\right)\right)\to x\in 𝒫B$$
11	2 9 10	uun0.1	$$⊢\left(A\subseteq B\wedge x\in 𝒫A\right)\to x\in 𝒫B$$
12	11	ex	$$⊢A\subseteq B\to \left(x\in 𝒫A\to x\in 𝒫B\right)$$
13	12	alrimiv	$$⊢A\subseteq B\to \forall x\left(x\in 𝒫A\to x\in 𝒫B\right)$$
14		dfss2	$$⊢𝒫A\subseteq 𝒫B\leftrightarrow \forall x\left(x\in 𝒫A\to x\in 𝒫B\right)$$
15	14	biimpri	$$⊢\forall x\left(x\in 𝒫A\to x\in 𝒫B\right)\to 𝒫A\subseteq 𝒫B$$
16	13 15	syl	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$
17	16	iin1	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$