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

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