Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sspwimpVD Structured version   Visualization version   GIF version

Theorem sspwimpVD 39469
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 39102) 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 39468 is sspwimpVD 39469 without virtual deductions and was derived from sspwimpVD 39469. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
 1:: ⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   ) 2:: ⊢ (    .............. 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ∈ 𝒫 𝐴   ) 3:2: ⊢ (    .............. 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ⊆ 𝐴   ) 4:3,1: ⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   ) 5:: ⊢ 𝑥 ∈ V 6:4,5: ⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵    ) 7:6: ⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)    ) 8:7: ⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   ) 9:8: ⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   ) qed:9: ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
Assertion
Ref Expression
sspwimpVD (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Proof of Theorem sspwimpVD
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 vex 3234 . . . . . . 7 𝑥 ∈ V
21vd01 39139 . . . . . 6 (      ▶   𝑥 ∈ V   )
3 idn1 39107 . . . . . . 7 (   𝐴𝐵   ▶   𝐴𝐵   )
4 idn1 39107 . . . . . . . 8 (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ∈ 𝒫 𝐴   )
5 elpwi 4201 . . . . . . . 8 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
64, 5el1 39170 . . . . . . 7 (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥𝐴   )
7 sstr 3644 . . . . . . . 8 ((𝑥𝐴𝐴𝐵) → 𝑥𝐵)
87ancoms 468 . . . . . . 7 ((𝐴𝐵𝑥𝐴) → 𝑥𝐵)
93, 6, 8el12 39270 . . . . . 6 (   (   𝐴𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥𝐵   )
102, 9elpwgdedVD 39467 . . . . . 6 (   (      ,   (   𝐴𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   )   ▶   𝑥 ∈ 𝒫 𝐵   )
112, 9, 10un0.1 39323 . . . . 5 (   (   𝐴𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵   )
1211int2 39148 . . . 4 (   𝐴𝐵   ▶   (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵)   )
1312gen11 39158 . . 3 (   𝐴𝐵   ▶   𝑥(𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵)   )
14 dfss2 3624 . . . 4 (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵))
1514biimpri 218 . . 3 (∀𝑥(𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵)
1613, 15el1 39170 . 2 (   𝐴𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
1716in1 39104 1 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1521  ⊤wtru 1524   ∈ wcel 2030  Vcvv 3231   ⊆ wss 3607  𝒫 cpw 4191  (   wvhc2 39113 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-pw 4193  df-vd1 39103  df-vhc2 39114 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator