Metamath Proof Explorer

Theorem sspwimpVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) using conjunction-form virtual hypothesis collections. It was completed manually, but has the potential to be completed automatically by a tools program which would invoke Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimp is sspwimpVD without virtual deductions and was derived from sspwimpVD . (Contributed by Alan Sare, 23-Apr-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 sspwimpVD ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 1 vd01 ⊢ (    ⊤    ▶    𝑥 ∈ V    )
3 idn1 ⊢ (    𝐴 ⊆ 𝐵    ▶    𝐴 ⊆ 𝐵    )
4 idn1 ⊢ (    𝑥 ∈ 𝒫 𝐴    ▶    𝑥 ∈ 𝒫 𝐴    )
5 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
6 4 5 el1 ⊢ (    𝑥 ∈ 𝒫 𝐴    ▶    𝑥 ⊆ 𝐴    )
7 sstr ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝑥 ⊆ 𝐵 )
8 7 ancoms ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ⊆ 𝐵 )
9 3 6 8 el12 ⊢ (    (    𝐴 ⊆ 𝐵    ,    𝑥 ∈ 𝒫 𝐴    )    ▶    𝑥 ⊆ 𝐵    )
10 2 9 elpwgdedVD ⊢ (    (    ⊤    ,    (    𝐴 ⊆ 𝐵    ,    𝑥 ∈ 𝒫 𝐴    )    )    ▶    𝑥 ∈ 𝒫 𝐵    )
11 2 9 10 un0.1 ⊢ (    (    𝐴 ⊆ 𝐵    ,    𝑥 ∈ 𝒫 𝐴    )    ▶    𝑥 ∈ 𝒫 𝐵    )
12 11 int2 ⊢ (    𝐴 ⊆ 𝐵    ▶    ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 )    )
13 12 gen11 ⊢ (    𝐴 ⊆ 𝐵    ▶    ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 )    )
14 dfss2 ⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) )
15 14 biimpri ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
16 13 15 el1 ⊢ (    𝐴 ⊆ 𝐵    ▶    𝒫 𝐴 ⊆ 𝒫 𝐵    )
17 16 in1 ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )