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

Theorem sspwimpVD 28440
Description: The following User's Proof is a Virtual Deduction proof ( see: wvd1 28065) 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 O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimp 28439 is sspwimpVD 28440 without virtual deductions and was derived from sspwimpVD 28440. (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 2867 . . . . . . 7  |-  x  e. 
_V
21vd01 28103 . . . . . 6  |-  (.  T.  ->.  x  e.  _V ).
3 idn1 28070 . . . . . . 7  |-  (. A  C_  B  ->.  A  C_  B ).
4 idn1 28070 . . . . . . . 8  |-  (. x  e.  ~P A  ->.  x  e.  ~P A ).
5 elpwi 3709 . . . . . . . 8  |-  ( x  e.  ~P A  ->  x  C_  A )
64, 5el1 28134 . . . . . . 7  |-  (. x  e.  ~P A  ->.  x  C_  A ).
7 sstr 3263 . . . . . . . 8  |-  ( ( x  C_  A  /\  A  C_  B )  ->  x  C_  B )
87ancoms 439 . . . . . . 7  |-  ( ( A  C_  B  /\  x  C_  A )  ->  x  C_  B )
93, 6, 8el12 28244 . . . . . 6  |-  (. (. A  C_  B ,. x  e.  ~P A ).  ->.  x  C_  B ).
102, 9elpwgdedVD 28438 . . . . . 6  |-  (. (.  T.  ,. (. A  C_  B ,. x  e.  ~P A ). ).  ->.  x  e.  ~P B ).
112, 9, 10un0.1 28297 . . . . 5  |-  (. (. A  C_  B ,. x  e.  ~P A ).  ->.  x  e.  ~P B ).
1211int2 28112 . . . 4  |-  (. A  C_  B  ->.  ( x  e. 
~P A  ->  x  e.  ~P B ) ).
1312gen11 28122 . . 3  |-  (. A  C_  B  ->.  A. x ( x  e.  ~P A  ->  x  e.  ~P B
) ).
14 dfss2 3245 . . . 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 28134 . 2  |-  (. A  C_  B  ->.  ~P A  C_  ~P B ).
1716in1 28067 1  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    T. wtru 1316   A.wal 1540    e. wcel 1710   _Vcvv 2864    C_ wss 3228   ~Pcpw 3701   (.wvhc2 28077
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235  df-ss 3242  df-pw 3703  df-vd1 28066  df-vhc2 28078
  Copyright terms: Public domain W3C validator