This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tskpwss

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

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

Proof

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