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

Metamath Proof Explorer

Theorem ptcls

Description: The closure of a box in the product topology is the box formed from the closures of the factors. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses ptcls.2 ⊢ 𝐽 = ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ 𝑅 ) )
ptcls.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ptcls.j ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
ptcls.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑆 ⊆ 𝑋 )
Assertion ptcls ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ X 𝑘 ∈ 𝐴 𝑆 ) = X 𝑘 ∈ 𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ptcls.2 ⊢ 𝐽 = ( ∏t ‘ ( 𝑘 ∈ 𝐴 ↦ 𝑅 ) )
2 ptcls.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 ptcls.j ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
4 ptcls.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑆 ⊆ 𝑋 )
5 toponmax ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝑅 )
6 3 5 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝑅 )
7 6 4 ssexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑆 ∈ V )
8 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝑆 ∈ V )
9 iunexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 𝑆 ∈ V ) → ∪ 𝑘 ∈ 𝐴 𝑆 ∈ V )
10 2 8 9 syl2anc ⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝑆 ∈ V )
11 axac3 ⊢ CHOICE
12 acacni ⊢ ( ( CHOICE ∧ 𝐴 ∈ 𝑉 ) → AC 𝐴 = V )
13 11 2 12 sylancr ⊢ ( 𝜑 → AC 𝐴 = V )
14 10 13 eleqtrrd ⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝑆 ∈ AC 𝐴 )
15 1 2 3 4 14 ptclsg ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ X 𝑘 ∈ 𝐴 𝑆 ) = X 𝑘 ∈ 𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )