Metamath Proof Explorer


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 dfss2 ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵 ) )
15 14 biimpri ( ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵 ) → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
16 13 15 syl ( 𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
17 16 iin1 ( 𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )