Theorem sspwtr

Description: Virtual deduction proof of the right-to-left implication of dftr4 . A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr without accumulating results. (Contributed by Alan Sare, 2-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sspwtr	|- ( 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		idn1	|- (. A C_ ~P A ->. A C_ ~P A ).
3		idn2	|- (. A C_ ~P A ,. ( z e. y /\ y e. A ) ->. ( z e. y /\ y e. A ) ).
4		simpr	|- ( ( z e. y /\ y e. A ) -> y e. A )
5	3 4	e2	|- (. A C_ ~P A ,. ( z e. y /\ y e. A ) ->. y e. A ).
6		ssel	|- ( A C_ ~P A -> ( y e. A -> y e. ~P A ) )
7	2 5 6	e12	|- (. A C_ ~P A ,. ( z e. y /\ y e. A ) ->. y e. ~P A ).
8		elpwi	|- ( y e. ~P A -> y C_ A )
9	7 8	e2	|- (. A C_ ~P A ,. ( z e. y /\ y e. A ) ->. y C_ A ).
10		simpl	|- ( ( z e. y /\ y e. A ) -> z e. y )
11	3 10	e2	|- (. A C_ ~P A ,. ( z e. y /\ y e. A ) ->. z e. y ).
12		ssel	|- ( y C_ A -> ( z e. y -> z e. A ) )
13	9 11 12	e22	|- (. A C_ ~P A ,. ( z e. y /\ y e. A ) ->. z e. A ).
14	13	in2	|- (. A C_ ~P A ->. ( ( z e. y /\ y e. A ) -> z e. A ) ).
15	14	gen12	|- (. A C_ ~P A ->. A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ).
16		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 ) )
17	1 15 16	e01	|- (. A C_ ~P A ->. Tr A ).
18	17	in1	|- ( A C_ ~P A -> Tr A )