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 ‘ 𝑅 ) ‘ 𝑆 ) )