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

Theorem sspwimpVD 43451
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 43101) 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 43450 is sspwimpVD 43451 without virtual deductions and was derived from sspwimpVD 43451. (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 3477 . . . . . . 7 𝑥 ∈ V
21vd01 43129 . . . . . 6 (      ▶   𝑥 ∈ V   )
3 idn1 43106 . . . . . . 7 (   𝐴𝐵   ▶   𝐴𝐵   )
4 idn1 43106 . . . . . . . 8 (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ∈ 𝒫 𝐴   )
5 elpwi 4603 . . . . . . . 8 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
64, 5el1 43160 . . . . . . 7 (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥𝐴   )
7 sstr 3986 . . . . . . . 8 ((𝑥𝐴𝐴𝐵) → 𝑥𝐵)
87ancoms 459 . . . . . . 7 ((𝐴𝐵𝑥𝐴) → 𝑥𝐵)
93, 6, 8el12 43258 . . . . . 6 (   (   𝐴𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥𝐵   )
102, 9elpwgdedVD 43449 . . . . . 6 (   (      ,   (   𝐴𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   )   ▶   𝑥 ∈ 𝒫 𝐵   )
112, 9, 10un0.1 43311 . . . . 5 (   (   𝐴𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵   )
1211int2 43138 . . . 4 (   𝐴𝐵   ▶   (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵)   )
1312gen11 43148 . . 3 (   𝐴𝐵   ▶   𝑥(𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵)   )
14 dfss2 3964 . . . 4 (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵))
1514biimpri 227 . . 3 (∀𝑥(𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵)
1613, 15el1 43160 . 2 (   𝐴𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
1716in1 43103 1 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1539  wtru 1542  wcel 2106  Vcvv 3473  wss 3944  𝒫 cpw 4596  (   wvhc2 43112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961  df-pw 4598  df-vd1 43102  df-vhc2 43113
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator