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 ) |