Step |
Hyp |
Ref |
Expression |
1 |
|
ptcldmpt.a |
|- ( ph -> A e. V ) |
2 |
|
ptcldmpt.j |
|- ( ( ph /\ k e. A ) -> J e. Top ) |
3 |
|
ptcldmpt.c |
|- ( ( ph /\ k e. A ) -> C e. ( Clsd ` J ) ) |
4 |
|
nfcv |
|- F/_ l C |
5 |
|
nfcsb1v |
|- F/_ k [_ l / k ]_ C |
6 |
|
csbeq1a |
|- ( k = l -> C = [_ l / k ]_ C ) |
7 |
4 5 6
|
cbvixp |
|- X_ k e. A C = X_ l e. A [_ l / k ]_ C |
8 |
2
|
fmpttd |
|- ( ph -> ( k e. A |-> J ) : A --> Top ) |
9 |
|
nfv |
|- F/ k ( ph /\ l e. A ) |
10 |
|
nfcv |
|- F/_ k Clsd |
11 |
|
nffvmpt1 |
|- F/_ k ( ( k e. A |-> J ) ` l ) |
12 |
10 11
|
nffv |
|- F/_ k ( Clsd ` ( ( k e. A |-> J ) ` l ) ) |
13 |
5 12
|
nfel |
|- F/ k [_ l / k ]_ C e. ( Clsd ` ( ( k e. A |-> J ) ` l ) ) |
14 |
9 13
|
nfim |
|- F/ k ( ( ph /\ l e. A ) -> [_ l / k ]_ C e. ( Clsd ` ( ( k e. A |-> J ) ` l ) ) ) |
15 |
|
eleq1w |
|- ( k = l -> ( k e. A <-> l e. A ) ) |
16 |
15
|
anbi2d |
|- ( k = l -> ( ( ph /\ k e. A ) <-> ( ph /\ l e. A ) ) ) |
17 |
|
2fveq3 |
|- ( k = l -> ( Clsd ` ( ( k e. A |-> J ) ` k ) ) = ( Clsd ` ( ( k e. A |-> J ) ` l ) ) ) |
18 |
6 17
|
eleq12d |
|- ( k = l -> ( C e. ( Clsd ` ( ( k e. A |-> J ) ` k ) ) <-> [_ l / k ]_ C e. ( Clsd ` ( ( k e. A |-> J ) ` l ) ) ) ) |
19 |
16 18
|
imbi12d |
|- ( k = l -> ( ( ( ph /\ k e. A ) -> C e. ( Clsd ` ( ( k e. A |-> J ) ` k ) ) ) <-> ( ( ph /\ l e. A ) -> [_ l / k ]_ C e. ( Clsd ` ( ( k e. A |-> J ) ` l ) ) ) ) ) |
20 |
|
simpr |
|- ( ( ph /\ k e. A ) -> k e. A ) |
21 |
|
eqid |
|- ( k e. A |-> J ) = ( k e. A |-> J ) |
22 |
21
|
fvmpt2 |
|- ( ( k e. A /\ J e. Top ) -> ( ( k e. A |-> J ) ` k ) = J ) |
23 |
20 2 22
|
syl2anc |
|- ( ( ph /\ k e. A ) -> ( ( k e. A |-> J ) ` k ) = J ) |
24 |
23
|
fveq2d |
|- ( ( ph /\ k e. A ) -> ( Clsd ` ( ( k e. A |-> J ) ` k ) ) = ( Clsd ` J ) ) |
25 |
3 24
|
eleqtrrd |
|- ( ( ph /\ k e. A ) -> C e. ( Clsd ` ( ( k e. A |-> J ) ` k ) ) ) |
26 |
14 19 25
|
chvarfv |
|- ( ( ph /\ l e. A ) -> [_ l / k ]_ C e. ( Clsd ` ( ( k e. A |-> J ) ` l ) ) ) |
27 |
1 8 26
|
ptcld |
|- ( ph -> X_ l e. A [_ l / k ]_ C e. ( Clsd ` ( Xt_ ` ( k e. A |-> J ) ) ) ) |
28 |
7 27
|
eqeltrid |
|- ( ph -> X_ k e. A C e. ( Clsd ` ( Xt_ ` ( k e. A |-> J ) ) ) ) |