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

Theorem sspwtrALT2 32712
Description: Short predicate calculus proof of the right-to-left implication of dftr4 4545. A class which is a subclass of its power class is transitive. This proof was constructed by applying Metamath's minimize command to the proof of sspwtrALT 32709, which is the virtual deduction proof sspwtr 32708 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sspwtrALT2  |-  ( A 
C_  ~P A  ->  Tr  A )

Proof of Theorem sspwtrALT2
Dummy variables  z 
y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3498 . . . . . 6  |-  ( A 
C_  ~P A  ->  (
y  e.  A  -> 
y  e.  ~P A
) )
21adantld 467 . . . . 5  |-  ( A 
C_  ~P A  ->  (
( z  e.  y  /\  y  e.  A
)  ->  y  e.  ~P A ) )
3 elpwi 4019 . . . . 5  |-  ( y  e.  ~P A  -> 
y  C_  A )
42, 3syl6 33 . . . 4  |-  ( A 
C_  ~P A  ->  (
( z  e.  y  /\  y  e.  A
)  ->  y  C_  A ) )
5 simpl 457 . . . . 5  |-  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  y )
65a1i 11 . . . 4  |-  ( A 
C_  ~P A  ->  (
( z  e.  y  /\  y  e.  A
)  ->  z  e.  y ) )
7 ssel 3498 . . . 4  |-  ( y 
C_  A  ->  (
z  e.  y  -> 
z  e.  A ) )
84, 6, 7syl6c 64 . . 3  |-  ( A 
C_  ~P A  ->  (
( z  e.  y  /\  y  e.  A
)  ->  z  e.  A ) )
98alrimivv 1696 . 2  |-  ( A 
C_  ~P A  ->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
10 dftr2 4542 . 2  |-  ( Tr  A  <->  A. z A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
119, 10sylibr 212 1  |-  ( A 
C_  ~P A  ->  Tr  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1377    e. wcel 1767    C_ wss 3476   ~Pcpw 4010   Tr wtr 4540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012  df-uni 4246  df-tr 4541
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator