This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 1 a1i ⊢ ( ⊤ → 𝑥 ∈ V )
3 id ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐵 )
4 id ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐴 )
5 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
6 4 5 syl ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
7 sstr ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝑥 ⊆ 𝐵 )
8 7 ancoms ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ⊆ 𝐵 )
9 3 6 8 syl2an ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ⊆ 𝐵 )
10 2 9 elpwgded ⊢ ( ( ⊤ ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴 ) ) → 𝑥 ∈ 𝒫 𝐵 )
11 2 9 10 uun0.1 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ∈ 𝒫 𝐵 )
12 11 ex ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) )
13 12 alrimiv ⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) )
14 df-ss ⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) )
15 14 biimpri ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
16 13 15 syl ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
17 16 iin1 ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )