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 V$
2	1	a1i	$⊢ ⊤ \to x \in 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	$⊢ (x \subseteq A \land A \subseteq B) \to x \subseteq B$
8	7	ancoms	$⊢ (A \subseteq B \land x \subseteq A) \to x \subseteq B$
9	3 6 8	syl2an	$⊢ (A \subseteq B \land x \in 𝒫 A) \to x \subseteq B$
10	2 9	elpwgded	$⊢ (⊤ \land (A \subseteq B \land x \in 𝒫 A)) \to x \in 𝒫 B$
11	2 9 10	uun0.1	$⊢ (A \subseteq B \land x \in 𝒫 A) \to x \in 𝒫 B$
12	11	ex	$⊢ A \subseteq B \to (x \in 𝒫 A \to x \in 𝒫 B)$
13	12	alrimiv	$⊢ A \subseteq B \to \forall x (x \in 𝒫 A \to x \in 𝒫 B)$
14		df-ss	$⊢ 𝒫 A \subseteq 𝒫 B \leftrightarrow \forall x (x \in 𝒫 A \to x \in 𝒫 B)$
15	14	biimpri	$⊢ \forall x (x \in 𝒫 A \to x \in 𝒫 B) \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$

Metamath Proof Explorer

Theorem sspwimp

Proof