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 44939
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 44589) 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 44938 is sspwimpVD 44939 without virtual deductions and was derived from sspwimpVD 44939. (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 3484 . . . . . . 7 𝑥 ∈ V
21vd01 44617 . . . . . 6 (      ▶   𝑥 ∈ V   )
3 idn1 44594 . . . . . . 7 (   𝐴𝐵   ▶   𝐴𝐵   )
4 idn1 44594 . . . . . . . 8 (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ∈ 𝒫 𝐴   )
5 elpwi 4607 . . . . . . . 8 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
64, 5el1 44648 . . . . . . 7 (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥𝐴   )
7 sstr 3992 . . . . . . . 8 ((𝑥𝐴𝐴𝐵) → 𝑥𝐵)
87ancoms 458 . . . . . . 7 ((𝐴𝐵𝑥𝐴) → 𝑥𝐵)
93, 6, 8el12 44746 . . . . . 6 (   (   𝐴𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥𝐵   )
102, 9elpwgdedVD 44937 . . . . . 6 (   (      ,   (   𝐴𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   )   ▶   𝑥 ∈ 𝒫 𝐵   )
112, 9, 10un0.1 44799 . . . . 5 (   (   𝐴𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵   )
1211int2 44626 . . . 4 (   𝐴𝐵   ▶   (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵)   )
1312gen11 44636 . . 3 (   𝐴𝐵   ▶   𝑥(𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵)   )
14 df-ss 3968 . . . 4 (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵))
1514biimpri 228 . . 3 (∀𝑥(𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵)
1613, 15el1 44648 . 2 (   𝐴𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
1716in1 44591 1 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538  wtru 1541  wcel 2108  Vcvv 3480  wss 3951  𝒫 cpw 4600  (   wvhc2 44600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-pw 4602  df-vd1 44590  df-vhc2 44601
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator