Metamath Proof Explorer

Theorem sspwimpcfVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) using conjunction-form virtual hypothesis collections. It was completed automatically by a tools program which would invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimpcf is sspwimpcfVD without virtual deductions and was derived from sspwimpcfVD . The version of completeusersproof.cmd used is capable of only generating conjunction-form unification theorems, not unification deductions. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

1:: |- (. A C_ B ->. A C_ B ).
2:: |- (. ........... x e. ~P A ->. x e. ~P A ).
3:2: |- (. ........... x e. ~P A ->. x C_ A ).
4:3,1: |- (. (. A C_ B ,. x e. ~P A ). ->. x C_ B ).
5:: |- x e.V
6:4,5: |- (. (. A C B ,. x e. ~P A ). ->. x e. ~P B ).
7:6: |- (. A C_ B ->. ( x e. ~P A -> x e. ~P B ) ).
8:7: |- (. A C_ B ->. A. x ( x e. ~P A -> x e. ~P B ) ).
9:8: |- (. A C_ B ->. ~P A C_ ~P B ).
qed:9: |- ( A C_ B -> ~P A C_ ~P B )

Ref Expression
Assertion sspwimpcfVD ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 idn1 ⊢ (    𝐴 ⊆ 𝐵    ▶    𝐴 ⊆ 𝐵    )
3 idn1 ⊢ (    𝑥 ∈ 𝒫 𝐴    ▶    𝑥 ∈ 𝒫 𝐴    )
4 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
5 3 4 el1 ⊢ (    𝑥 ∈ 𝒫 𝐴    ▶    𝑥 ⊆ 𝐴    )
6 sstr2 ⊢ ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵 ) )
7 6 impcom ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ⊆ 𝐵 )
8 2 5 7 el12 ⊢ (    (    𝐴 ⊆ 𝐵    ,    𝑥 ∈ 𝒫 𝐴    )    ▶    𝑥 ⊆ 𝐵    )
9 elpwg ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 ) )
10 9 biimpar ⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ∈ 𝒫 𝐵 )
11 1 8 10 el021old ⊢ (    (    𝐴 ⊆ 𝐵    ,    𝑥 ∈ 𝒫 𝐴    )    ▶    𝑥 ∈ 𝒫 𝐵    )
12 11 int2 ⊢ (    𝐴 ⊆ 𝐵    ▶    ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 )    )
13 12 gen11 ⊢ (    𝐴 ⊆ 𝐵    ▶    ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 )    )
14 dfss2 ⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) )
15 14 biimpri ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
16 13 15 el1 ⊢ (    𝐴 ⊆ 𝐵    ▶    𝒫 𝐴 ⊆ 𝒫 𝐵    )
17 16 in1 ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )