Theorem trsspwALT2

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

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

Proof

Step	Hyp	Ref	Expression
1		dfss2	|- ( A C_ ~P A <-> A. x ( x e. A -> x e. ~P A ) )
2		id	|- ( Tr A -> Tr A )
3		idd	|- ( Tr A -> ( x e. A -> x e. A ) )
4		trss	|- ( Tr A -> ( x e. A -> x C_ A ) )
5	2 3 4	sylsyld	|- ( Tr A -> ( x e. A -> x C_ A ) )
6		vex	|- x e. _V
7	6	elpw	|- ( x e. ~P A <-> x C_ A )
8	5 7	syl6ibr	|- ( Tr A -> ( x e. A -> x e. ~P A ) )
9	8	idiALT	|- ( Tr A -> ( x e. A -> x e. ~P A ) )
10	9	alrimiv	|- ( Tr A -> A. x ( x e. A -> x e. ~P A ) )
11		biimpr	|- ( ( A C_ ~P A <-> A. x ( x e. A -> x e. ~P A ) ) -> ( A. x ( x e. A -> x e. ~P A ) -> A C_ ~P A ) )
12	1 10 11	mpsyl	|- ( Tr A -> A C_ ~P A )
13	12	idiALT	|- ( Tr A -> A C_ ~P A )