sspwimpcf

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. sspwimpcf , using conventional notation, was translated from its virtual deduction form, sspwimpcfVD , using a translation program. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		id	$⊢ A \subseteq B \to A \subseteq B$
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		sstr2	$⊢ x \subseteq A \to (A \subseteq B \to x \subseteq B)$
7	6	impcom	$⊢ (A \subseteq B \land x \subseteq A) \to x \subseteq B$
8	2 5 7	syl2an	$⊢ (A \subseteq B \land x \in 𝒫 A) \to x \subseteq B$
9		elpwg	$⊢ x \in V \to (x \in 𝒫 B \leftrightarrow x \subseteq B)$
10	9	biimpar	$⊢ (x \in V \land x \subseteq B) \to x \in 𝒫 B$
11	1 8 10	eel021old	$⊢ (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 sspwimpcf

Proof