Theorem tskpw

Description: Second axiom of a Tarski class. The powerset of an element of a Tarski class belongs to the class. (Contributed by FL, 30-Dec-2010) (Proof shortened by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	tskpw	|- ( ( T e. Tarski /\ A e. T ) -> ~P A e. T )

Proof

Step	Hyp	Ref	Expression
1		eltsk2g	|- ( T e. Tarski -> ( T e. Tarski <-> ( A. x e. T ( ~P x C_ T /\ ~P x e. T ) /\ A. x e. ~P T ( x ~~ T \/ x e. T ) ) ) )
2	1	ibi	|- ( T e. Tarski -> ( A. x e. T ( ~P x C_ T /\ ~P x e. T ) /\ A. x e. ~P T ( x ~~ T \/ x e. T ) ) )
3	2	simpld	|- ( T e. Tarski -> A. x e. T ( ~P x C_ T /\ ~P x e. T ) )
4		simpr	|- ( ( ~P x C_ T /\ ~P x e. T ) -> ~P x e. T )
5	4	ralimi	|- ( A. x e. T ( ~P x C_ T /\ ~P x e. T ) -> A. x e. T ~P x e. T )
6	3 5	syl	|- ( T e. Tarski -> A. x e. T ~P x e. T )
7		pweq	|- ( x = A -> ~P x = ~P A )
8	7	eleq1d	|- ( x = A -> ( ~P x e. T <-> ~P A e. T ) )
9	8	rspccva	|- ( ( A. x e. T ~P x e. T /\ A e. T ) -> ~P A e. T )
10	6 9	sylan	|- ( ( T e. Tarski /\ A e. T ) -> ~P A e. T )