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