Metamath Proof Explorer

Theorem pwtrrVD

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

Ref Expression
Hypothesis pwtrrVD.1 
|- A e. _V
Assertion pwtrrVD 
|- ( Tr ~P A -> Tr A )

Proof

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