Metamath Proof Explorer


Theorem ptcldmpt

Description: A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypotheses ptcldmpt.a
|- ( ph -> A e. V )
ptcldmpt.j
|- ( ( ph /\ k e. A ) -> J e. Top )
ptcldmpt.c
|- ( ( ph /\ k e. A ) -> C e. ( Clsd ` J ) )
Assertion ptcldmpt
|- ( ph -> X_ k e. A C e. ( Clsd ` ( Xt_ ` ( k e. A |-> J ) ) ) )

Proof

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