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.

Step	Hyp	Ref	Expression
1		vex 3112	. . . . . . 7 |- x e. _V
2	1	vd01 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 )
6	4, 5	el1 33557	. . . . . . 7 |- (. x e. ~P A ->. x C_ A ).
7		sstr 3507	. . . . . . . 8 |- ( ( x C_ A /\ A C_ B ) -> x C_ B )
8	7	ancoms 453	. . . . . . 7 |- ( ( A C_ B /\ x C_ A ) -> x C_ B )
9	3, 6, 8	el12 33666	. . . . . 6 |- (. (. A C_ B ,. x e. ~P A ). ->. x C_ B ).
10	2, 9	elpwgdedVD 33860	. . . . . 6 |- (. (. T. ,. (. A C_ B ,. x e. ~P A ). ). ->. x e. ~P B ).
11	2, 9, 10	un0.1 33719	. . . . 5 |- (. (. A C_ B ,. x e. ~P A ). ->. x e. ~P B ).
12	11	int2 33535	. . . 4 |- (. A C_ B ->. ( x e. ~P A -> x e. ~P B ) ).
13	12	gen11 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 ) )
15	14	biimpri 206	. . 3 |- ( A. x ( x e. ~P A -> x e. ~P B ) -> ~P A C_ ~P B )
16	13, 15	el1 33557	. 2 |- (. A C_ B ->. ~P A C_ ~P B ).
17	16	in1 33491	1 |- ( A C_ B -> ~P A C_ ~P B )

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)