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

Theorem sspwimpVD 33862
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 33489) 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 33861 is sspwimpVD 33862 without virtual deductions and was derived from sspwimpVD 33862. (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 )
Assertion
Ref Expression
sspwimpVD  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )

Proof of Theorem sspwimpVD
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 vex 3112 . . . . . . 7  |-  x  e. 
_V
21vd01 33526 . . . . . 6  |-  (. T.  ->.  x  e.  _V ).
3 idn1 33494 . . . . . . 7  |-  (. A  C_  B  ->.  A  C_  B ).
4 idn1 33494 . . . . . . . 8  |-  (. x  e.  ~P A  ->.  x  e.  ~P A ).
5 elpwi 4024 . . . . . . . 8  |-  ( x  e.  ~P A  ->  x  C_  A )
64, 5el1 33557 . . . . . . 7  |-  (. x  e.  ~P A  ->.  x  C_  A ).
7 sstr 3507 . . . . . . . 8  |-  ( ( x  C_  A  /\  A  C_  B )  ->  x  C_  B )
87ancoms 453 . . . . . . 7  |-  ( ( A  C_  B  /\  x  C_  A )  ->  x  C_  B )
93, 6, 8el12 33666 . . . . . 6  |-  (. (. A  C_  B ,. x  e.  ~P A ).  ->.  x  C_  B ).
102, 9elpwgdedVD 33860 . . . . . 6  |-  (. (. T.  ,. (. A  C_  B ,. x  e.  ~P A ). ).  ->.  x  e.  ~P B ).
112, 9, 10un0.1 33719 . . . . 5  |-  (. (. A  C_  B ,. x  e.  ~P A ).  ->.  x  e.  ~P B ).
1211int2 33535 . . . 4  |-  (. A  C_  B  ->.  ( x  e. 
~P A  ->  x  e.  ~P B ) ).
1312gen11 33545 . . 3  |-  (. A  C_  B  ->.  A. x ( x  e.  ~P A  ->  x  e.  ~P B
) ).
14 dfss2 3488 . . . 4  |-  ( ~P A  C_  ~P B  <->  A. x ( x  e. 
~P A  ->  x  e.  ~P B ) )
1514biimpri 206 . . 3  |-  ( A. x ( x  e. 
~P A  ->  x  e.  ~P B )  ->  ~P A  C_  ~P B
)
1613, 15el1 33557 . 2  |-  (. A  C_  B  ->.  ~P A  C_  ~P B ).
1716in1 33491 1  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1393   T. wtru 1396    e. wcel 1819   _Vcvv 3109    C_ wss 3471   ~Pcpw 4015   (.wvhc2 33500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478  df-ss 3485  df-pw 4017  df-vd1 33490  df-vhc2 33501
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator