Metamath Proof Explorer

Theorem pwtrVD

Description: Virtual deduction proof of pwtr ; see pwtrrVD for the converse. (Contributed by Alan Sare, 25-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pwtrVD 
|- ( Tr A -> Tr ~P A )

Proof

Step Hyp Ref Expression
1 dftr2 
 |-  ( Tr ~P A <-> A. z A. y ( ( z e. y /\ y e. ~P A ) -> z e. ~P A ) )
2 idn1 
 |-  (. Tr A ->. Tr A ).
3 idn2 
 |-  (. Tr A ,. ( z e. y /\ y e. ~P A ) ->. ( z e. y /\ y e. ~P A ) ).
4 simpr 
 |-  ( ( z e. y /\ y e. ~P A ) -> y e. ~P A )
5 3 4 e2 
 |-  (. Tr A ,. ( z e. y /\ y e. ~P A ) ->. y e. ~P A ).
6 elpwi 
 |-  ( y e. ~P A -> y C_ A )
7 5 6 e2 
 |-  (. Tr A ,. ( z e. y /\ y e. ~P A ) ->. y C_ A ).
8 simpl 
 |-  ( ( z e. y /\ y e. ~P A ) -> z e. y )
9 3 8 e2 
 |-  (. Tr A ,. ( z e. y /\ y e. ~P A ) ->. z e. y ).
10 ssel 
 |-  ( y C_ A -> ( z e. y -> z e. A ) )
11 7 9 10 e22 
 |-  (. Tr A ,. ( z e. y /\ y e. ~P A ) ->. z e. A ).
12 trss 
 |-  ( Tr A -> ( z e. A -> z C_ A ) )
13 2 11 12 e12 
 |-  (. Tr A ,. ( z e. y /\ y e. ~P A ) ->. z C_ A ).
14 vex 
 |-  z e. _V
15 14 elpw 
 |-  ( z e. ~P A <-> z C_ A )
16 13 15 e2bir 
 |-  (. Tr A ,. ( z e. y /\ y e. ~P A ) ->. z e. ~P A ).
17 16 in2 
 |-  (. Tr A ->. ( ( z e. y /\ y e. ~P A ) -> z e. ~P A ) ).
18 17 gen12 
 |-  (. Tr A ->. A. z A. y ( ( z e. y /\ y e. ~P A ) -> z e. ~P A ) ).
19 biimpr 
 |-  ( ( Tr ~P A <-> A. z A. y ( ( z e. y /\ y e. ~P A ) -> z e. ~P A ) ) -> ( A. z A. y ( ( z e. y /\ y e. ~P A ) -> z e. ~P A ) -> Tr ~P A ) )
20 1 18 19 e01 
 |-  (. Tr A ->. Tr ~P A ).
21 20 in1 
 |-  ( Tr A -> Tr ~P A )