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	|- J = ( Xt_ ` ( k e. A |-> R ) )
	ptcls.a	|- ( ph -> A e. V )
	ptcls.j	|- ( ( ph /\ k e. A ) -> R e. ( TopOn ` X ) )
	ptcls.c	|- ( ( ph /\ k e. A ) -> S C_ X )
Assertion	ptcls	|- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )

Proof

Step	Hyp	Ref	Expression
1		ptcls.2	|- J = ( Xt_ ` ( k e. A |-> R ) )
2		ptcls.a	|- ( ph -> A e. V )
3		ptcls.j	|- ( ( ph /\ k e. A ) -> R e. ( TopOn ` X ) )
4		ptcls.c	|- ( ( ph /\ k e. A ) -> S C_ X )
5		toponmax	|- ( R e. ( TopOn ` X ) -> X e. R )
6	3 5	syl	|- ( ( ph /\ k e. A ) -> X e. R )
7	6 4	ssexd	|- ( ( ph /\ k e. A ) -> S e. _V )
8	7	ralrimiva	|- ( ph -> A. k e. A S e. _V )
9		iunexg	|- ( ( A e. V /\ A. k e. A S e. _V ) -> U_ k e. A S e. _V )
10	2 8 9	syl2anc	|- ( ph -> U_ k e. A S e. _V )
11		axac3	|- CHOICE
12		acacni	|- ( ( CHOICE /\ A e. V ) -> AC_ A = _V )
13	11 2 12	sylancr	|- ( ph -> AC_ A = _V )
14	10 13	eleqtrrd	|- ( ph -> U_ k e. A S e. AC_ A )
15	1 2 3 4 14	ptclsg	|- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )