Theorem sspwimpALT

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. sspwimpALT is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html . It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 9 used elpwgded ). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 5 used elpwi ). (Contributed by Alan Sare, 3-Dec-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sspwimpALT	$$⊢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	$$⊢x\in 𝒫A\to x\in 𝒫A$$
4		elpwi	$$⊢x\in 𝒫A\to x\subseteq A$$
5	3 4	syl	$$⊢x\in 𝒫A\to x\subseteq A$$
6		id	$$⊢A\subseteq B\to A\subseteq B$$
7	5 6	sylan9ssr	$$⊢\left(A\subseteq B\wedge x\in 𝒫A\right)\to x\subseteq B$$
8	2 7	elpwgded	$$⊢\left(\top \wedge \left(A\subseteq B\wedge x\in 𝒫A\right)\right)\to x\in 𝒫B$$
9	8	uunT1	$$⊢\left(A\subseteq B\wedge x\in 𝒫A\right)\to x\in 𝒫B$$
10	9	ex	$$⊢A\subseteq B\to \left(x\in 𝒫A\to x\in 𝒫B\right)$$
11	10	alrimiv	$$⊢A\subseteq B\to \forall x\left(x\in 𝒫A\to x\in 𝒫B\right)$$
12		df-ss	$$⊢𝒫A\subseteq 𝒫B\leftrightarrow \forall x\left(x\in 𝒫A\to x\in 𝒫B\right)$$
13	12	biimpri	$$⊢\forall x\left(x\in 𝒫A\to x\in 𝒫B\right)\to 𝒫A\subseteq 𝒫B$$
14	11 13	syl	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$
15	14	idiALT	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$