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 
|- 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 ) )