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 ( 𝜑𝐴𝑉 )
ptcldmpt.j ( ( 𝜑𝑘𝐴 ) → 𝐽 ∈ Top )
ptcldmpt.c ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ( Clsd ‘ 𝐽 ) )
Assertion ptcldmpt ( 𝜑X 𝑘𝐴 𝐶 ∈ ( Clsd ‘ ( ∏t ‘ ( 𝑘𝐴𝐽 ) ) ) )

Proof

Step Hyp Ref Expression
1 ptcldmpt.a ( 𝜑𝐴𝑉 )
2 ptcldmpt.j ( ( 𝜑𝑘𝐴 ) → 𝐽 ∈ Top )
3 ptcldmpt.c ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ( Clsd ‘ 𝐽 ) )
4 nfcv 𝑙 𝐶
5 nfcsb1v 𝑘 𝑙 / 𝑘 𝐶
6 csbeq1a ( 𝑘 = 𝑙𝐶 = 𝑙 / 𝑘 𝐶 )
7 4 5 6 cbvixp X 𝑘𝐴 𝐶 = X 𝑙𝐴 𝑙 / 𝑘 𝐶
8 2 fmpttd ( 𝜑 → ( 𝑘𝐴𝐽 ) : 𝐴 ⟶ Top )
9 nfv 𝑘 ( 𝜑𝑙𝐴 )
10 nfcv 𝑘 Clsd
11 nffvmpt1 𝑘 ( ( 𝑘𝐴𝐽 ) ‘ 𝑙 )
12 10 11 nffv 𝑘 ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑙 ) )
13 5 12 nfel 𝑘 𝑙 / 𝑘 𝐶 ∈ ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑙 ) )
14 9 13 nfim 𝑘 ( ( 𝜑𝑙𝐴 ) → 𝑙 / 𝑘 𝐶 ∈ ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑙 ) ) )
15 eleq1w ( 𝑘 = 𝑙 → ( 𝑘𝐴𝑙𝐴 ) )
16 15 anbi2d ( 𝑘 = 𝑙 → ( ( 𝜑𝑘𝐴 ) ↔ ( 𝜑𝑙𝐴 ) ) )
17 2fveq3 ( 𝑘 = 𝑙 → ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑘 ) ) = ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑙 ) ) )
18 6 17 eleq12d ( 𝑘 = 𝑙 → ( 𝐶 ∈ ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑘 ) ) ↔ 𝑙 / 𝑘 𝐶 ∈ ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑙 ) ) ) )
19 16 18 imbi12d ( 𝑘 = 𝑙 → ( ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑘 ) ) ) ↔ ( ( 𝜑𝑙𝐴 ) → 𝑙 / 𝑘 𝐶 ∈ ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑙 ) ) ) ) )
20 simpr ( ( 𝜑𝑘𝐴 ) → 𝑘𝐴 )
21 eqid ( 𝑘𝐴𝐽 ) = ( 𝑘𝐴𝐽 )
22 21 fvmpt2 ( ( 𝑘𝐴𝐽 ∈ Top ) → ( ( 𝑘𝐴𝐽 ) ‘ 𝑘 ) = 𝐽 )
23 20 2 22 syl2anc ( ( 𝜑𝑘𝐴 ) → ( ( 𝑘𝐴𝐽 ) ‘ 𝑘 ) = 𝐽 )
24 23 fveq2d ( ( 𝜑𝑘𝐴 ) → ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑘 ) ) = ( Clsd ‘ 𝐽 ) )
25 3 24 eleqtrrd ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑘 ) ) )
26 14 19 25 chvarfv ( ( 𝜑𝑙𝐴 ) → 𝑙 / 𝑘 𝐶 ∈ ( Clsd ‘ ( ( 𝑘𝐴𝐽 ) ‘ 𝑙 ) ) )
27 1 8 26 ptcld ( 𝜑X 𝑙𝐴 𝑙 / 𝑘 𝐶 ∈ ( Clsd ‘ ( ∏t ‘ ( 𝑘𝐴𝐽 ) ) ) )
28 7 27 eqeltrid ( 𝜑X 𝑘𝐴 𝐶 ∈ ( Clsd ‘ ( ∏t ‘ ( 𝑘𝐴𝐽 ) ) ) )