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

Theorem sspwtrALT2 37213
Description: Short predicate calculus proof of the right-to-left implication of dftr4 4501. 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 37204, which is the virtual deduction proof sspwtr 37203 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 3425 . . . . . 6  |-  ( A 
C_  ~P A  ->  (
y  e.  A  -> 
y  e.  ~P A
) )
21adantld 469 . . . . 5  |-  ( A 
C_  ~P A  ->  (
( z  e.  y  /\  y  e.  A
)  ->  y  e.  ~P A ) )
3 elpwi 3959 . . . . 5  |-  ( y  e.  ~P A  -> 
y  C_  A )
42, 3syl6 34 . . . 4  |-  ( A 
C_  ~P A  ->  (
( z  e.  y  /\  y  e.  A
)  ->  y  C_  A ) )
5 simpl 459 . . . . 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 3425 . . . 4  |-  ( y 
C_  A  ->  (
z  e.  y  -> 
z  e.  A ) )
84, 6, 7syl6c 66 . . 3  |-  ( A 
C_  ~P A  ->  (
( z  e.  y  /\  y  e.  A
)  ->  z  e.  A ) )
98alrimivv 1773 . 2  |-  ( A 
C_  ~P A  ->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
10 dftr2 4498 . 2  |-  ( Tr  A  <->  A. z A. y
( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
119, 10sylibr 216 1  |-  ( A 
C_  ~P A  ->  Tr  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371   A.wal 1441    e. wcel 1886    C_ wss 3403   ~Pcpw 3950   Tr wtr 4496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-in 3410  df-ss 3417  df-pw 3952  df-uni 4198  df-tr 4497
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator