Theorem sspwtrALT

Description: Virtual deduction proof of sspwtr . This proof is the same as the proof of sspwtr except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A class which is a subclass of its power class is transitive. (Contributed by Alan Sare, 3-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dftr2	|- ( Tr A <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) )
2		simpr	|- ( ( z e. y /\ y e. A ) -> y e. A )
3		ssel	|- ( A C_ ~P A -> ( y e. A -> y e. ~P A ) )
4		elpwi	|- ( y e. ~P A -> y C_ A )
5	2 3 4	syl56	|- ( A C_ ~P A -> ( ( z e. y /\ y e. A ) -> y C_ A ) )
6		idd	|- ( A C_ ~P A -> ( ( z e. y /\ y e. A ) -> ( z e. y /\ y e. A ) ) )
7		simpl	|- ( ( z e. y /\ y e. A ) -> z e. y )
8	6 7	syl6	|- ( A C_ ~P A -> ( ( z e. y /\ y e. A ) -> z e. y ) )
9		ssel	|- ( y C_ A -> ( z e. y -> z e. A ) )
10	5 8 9	syl6c	|- ( A C_ ~P A -> ( ( z e. y /\ y e. A ) -> z e. A ) )
11	10	alrimivv	|- ( A C_ ~P A -> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) )
12		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 ) )
13	1 11 12	mpsyl	|- ( A C_ ~P A -> Tr A )
14	13	idiALT	|- ( A C_ ~P A -> Tr A )