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

Theorem sspwimpcfVD 29013
Description: The following User's Proof is a Virtual Deduction proof ( see: wvd1 28636) using conjunction-form virtual hypothesis collections. It was completed automatically by a tools program which would invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimpcf 29012 is sspwimpcfVD 29013 without virtual deductions and was derived from sspwimpcfVD 29013. 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 )
Assertion
Ref Expression
sspwimpcfVD  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )

Proof of Theorem sspwimpcfVD
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 vex 2804 . . . . . 6  |-  x  e. 
_V
2 idn1 28641 . . . . . . 7  |-  (. A  C_  B  ->.  A  C_  B ).
3 idn1 28641 . . . . . . . 8  |-  (. x  e.  ~P A  ->.  x  e.  ~P A ).
4 elpwi 3646 . . . . . . . 8  |-  ( x  e.  ~P A  ->  x  C_  A )
53, 4el1 28705 . . . . . . 7  |-  (. x  e.  ~P A  ->.  x  C_  A ).
6 sstr2 3199 . . . . . . . 8  |-  ( x 
C_  A  ->  ( A  C_  B  ->  x  C_  B ) )
76impcom 419 . . . . . . 7  |-  ( ( A  C_  B  /\  x  C_  A )  ->  x  C_  B )
82, 5, 7el12 28815 . . . . . 6  |-  (. (. A  C_  B ,. x  e.  ~P A ).  ->.  x  C_  B ).
9 elpwg 3645 . . . . . . 7  |-  ( x  e.  _V  ->  (
x  e.  ~P B  <->  x 
C_  B ) )
109biimpar 471 . . . . . 6  |-  ( ( x  e.  _V  /\  x  C_  B )  ->  x  e.  ~P B
)
111, 8, 10el021old 28779 . . . . 5  |-  (. (. A  C_  B ,. x  e.  ~P A ).  ->.  x  e.  ~P B ).
1211int2 28683 . . . 4  |-  (. A  C_  B  ->.  ( x  e. 
~P A  ->  x  e.  ~P B ) ).
1312gen11 28693 . . 3  |-  (. A  C_  B  ->.  A. x ( x  e.  ~P A  ->  x  e.  ~P B
) ).
14 dfss2 3182 . . . 4  |-  ( ~P A  C_  ~P B  <->  A. x ( x  e. 
~P A  ->  x  e.  ~P B ) )
1514biimpri 197 . . 3  |-  ( A. x ( x  e. 
~P A  ->  x  e.  ~P B )  ->  ~P A  C_  ~P B
)
1613, 15el1 28705 . 2  |-  (. A  C_  B  ->.  ~P A  C_  ~P B ).
1716in1 28638 1  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530    e. wcel 1696   _Vcvv 2801    C_ wss 3165   ~Pcpw 3638
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640  df-vd1 28637  df-vhc2 28649
  Copyright terms: Public domain W3C validator