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 = \prod_{𝑡} ((k \in A ⟼ R))$
		ptcls.a	$⊢ φ \to A \in V$
		ptcls.j	$⊢ (φ \land k \in A) \to R \in TopOn (X)$
		ptcls.c	$⊢ (φ \land k \in A) \to S \subseteq X$
	Assertion	ptcls	$⊢ φ \to cls (J) (\underset{k \in A}{⨉} S) = \underset{k \in A}{⨉} cls (R) (S)$

Proof

Step	Hyp	Ref	Expression
1		ptcls.2	$⊢ J = \prod_{𝑡} ((k \in A ⟼ R))$
2		ptcls.a	$⊢ φ \to A \in V$
3		ptcls.j	$⊢ (φ \land k \in A) \to R \in TopOn (X)$
4		ptcls.c	$⊢ (φ \land k \in A) \to S \subseteq X$
5		toponmax	$⊢ R \in TopOn (X) \to X \in R$
6	3 5	syl	$⊢ (φ \land k \in A) \to X \in R$
7	6 4	ssexd	$⊢ (φ \land k \in A) \to S \in V$
8	7	ralrimiva	$⊢ φ \to \forall k \in A S \in V$
9		iunexg	$⊢ (A \in V \land \forall k \in A S \in V) \to ⋃_{k \in A} S \in V$
10	2 8 9	syl2anc	$⊢ φ \to ⋃_{k \in A} S \in V$
11		axac3	$⊢ CHOICE$
12		acacni	$⊢ (CHOICE \land A \in V) \to \underline{AC} A = V$
13	11 2 12	sylancr	$⊢ φ \to \underline{AC} A = V$
14	10 13	eleqtrrd	$⊢ φ \to ⋃_{k \in A} S \in \underline{AC} A$
15	1 2 3 4 14	ptclsg	$⊢ φ \to cls (J) (\underset{k \in A}{⨉} S) = \underset{k \in A}{⨉} cls (R) (S)$