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 ⊢ φ → A ∈ V
ptcldmpt.j ⊢ φ ∧ k ∈ A → J ∈ Top
ptcldmpt.c ⊢ φ ∧ k ∈ A → C ∈ Clsd ⁡ J
Assertion ptcldmpt ⊢ φ → ⨉ k ∈ A C ∈ Clsd ⁡ ∏ 𝑡 ⁡ k ∈ A ⟼ J

Proof

Step Hyp Ref Expression
1 ptcldmpt.a ⊢ φ → A ∈ V
2 ptcldmpt.j ⊢ φ ∧ k ∈ A → J ∈ Top
3 ptcldmpt.c ⊢ φ ∧ k ∈ A → C ∈ Clsd ⁡ J
4 nfcv ⊢ Ⅎ _ l C
5 nfcsb1v ⊢ Ⅎ _ k ⦋ l / k⦌ C
6 csbeq1a ⊢ k = l → C = ⦋ l / k⦌ C
7 4 5 6 cbvixp ⊢ ⨉ k ∈ A C = ⨉ l ∈ A ⦋ l / k⦌ C
8 2 fmpttd ⊢ φ → k ∈ A ⟼ J : A ⟶ Top
9 nfv ⊢ Ⅎ k φ ∧ l ∈ A
10 nfcv ⊢ Ⅎ _ k Clsd
11 nffvmpt1 ⊢ Ⅎ _ k k ∈ A ⟼ J ⁡ l
12 10 11 nffv ⊢ Ⅎ _ k Clsd ⁡ k ∈ A ⟼ J ⁡ l
13 5 12 nfel ⊢ Ⅎ k ⦋ l / k⦌ C ∈ Clsd ⁡ k ∈ A ⟼ J ⁡ l
14 9 13 nfim ⊢ Ⅎ k φ ∧ l ∈ A → ⦋ l / k⦌ C ∈ Clsd ⁡ k ∈ A ⟼ J ⁡ l
15 eleq1w ⊢ k = l → k ∈ A ↔ l ∈ A
16 15 anbi2d ⊢ k = l → φ ∧ k ∈ A ↔ φ ∧ l ∈ A
17 2fveq3 ⊢ k = l → Clsd ⁡ k ∈ A ⟼ J ⁡ k = Clsd ⁡ k ∈ A ⟼ J ⁡ l
18 6 17 eleq12d ⊢ k = l → C ∈ Clsd ⁡ k ∈ A ⟼ J ⁡ k ↔ ⦋ l / k⦌ C ∈ Clsd ⁡ k ∈ A ⟼ J ⁡ l
19 16 18 imbi12d ⊢ k = l → φ ∧ k ∈ A → C ∈ Clsd ⁡ k ∈ A ⟼ J ⁡ k ↔ φ ∧ l ∈ A → ⦋ l / k⦌ C ∈ Clsd ⁡ k ∈ A ⟼ J ⁡ l
20 simpr ⊢ φ ∧ k ∈ A → k ∈ A
21 eqid ⊢ k ∈ A ⟼ J = k ∈ A ⟼ J
22 21 fvmpt2 ⊢ k ∈ A ∧ J ∈ Top → k ∈ A ⟼ J ⁡ k = J
23 20 2 22 syl2anc ⊢ φ ∧ k ∈ A → k ∈ A ⟼ J ⁡ k = J
24 23 fveq2d ⊢ φ ∧ k ∈ A → Clsd ⁡ k ∈ A ⟼ J ⁡ k = Clsd ⁡ J
25 3 24 eleqtrrd ⊢ φ ∧ k ∈ A → C ∈ Clsd ⁡ k ∈ A ⟼ J ⁡ k
26 14 19 25 chvarfv ⊢ φ ∧ l ∈ A → ⦋ l / k⦌ C ∈ Clsd ⁡ k ∈ A ⟼ J ⁡ l
27 1 8 26 ptcld ⊢ φ → ⨉ l ∈ A ⦋ l / k⦌ C ∈ Clsd ⁡ ∏ 𝑡 ⁡ k ∈ A ⟼ J
28 7 27 eqeltrid ⊢ φ → ⨉ k ∈ A C ∈ Clsd ⁡ ∏ 𝑡 ⁡ k ∈ A ⟼ J