Theorem sspwtrALT2

Description: Short predicate calculus proof of the right-to-left implication of dftr4 . 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 , which is the virtual deduction proof sspwtr without virtual deductions. (Contributed by Alan Sare, 3-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ssel	|- ( A C_ ~P A -> ( y e. A -> y e. ~P A ) )
2	1	adantld	|- ( A C_ ~P A -> ( ( z e. y /\ y e. A ) -> y e. ~P A ) )
3		elpwi	|- ( y e. ~P A -> y C_ A )
4	2 3	syl6	|- ( A C_ ~P A -> ( ( z e. y /\ y e. A ) -> y C_ A ) )
5		simpl	|- ( ( z e. y /\ y e. A ) -> z e. y )
6	5	a1i	|- ( A C_ ~P A -> ( ( z e. y /\ y e. A ) -> z e. y ) )
7		ssel	|- ( y C_ A -> ( z e. y -> z e. A ) )
8	4 6 7	syl6c	|- ( A C_ ~P A -> ( ( z e. y /\ y e. A ) -> z e. A ) )
9	8	alrimivv	|- ( A C_ ~P A -> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) )
10		dftr2	|- ( Tr A <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) )
11	9 10	sylibr	|- ( A C_ ~P A -> Tr A )