Theorem 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	⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		id	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐵 )
3		id	⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐴 )
4		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
5	3 4	syl	⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
6		sstr2	⊢ ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵 ) )
7	6	impcom	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ⊆ 𝐵 )
8	2 5 7	syl2an	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ⊆ 𝐵 )
9		elpwg	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 ) )
10	9	biimpar	⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ∈ 𝒫 𝐵 )
11	1 8 10	eel021old	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ∈ 𝒫 𝐵 )
12	11	ex	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) )
13	12	alrimiv	⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) )
14		df-ss	⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) )
15	14	biimpri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
16	13 15	syl	⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
17	16	iin1	⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )