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 ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐽 ) ) ) )