pttoponconst

Description: The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 22-Aug-2015)

		Ref	Expression
	Hypothesis	ptuniconst.2	$⊢ J = \prod_{𝑡} (A \times \{R\})$
	Assertion	pttoponconst	$⊢ (A \in V \land R \in TopOn (X)) \to J \in TopOn (X^{A})$

Step	Hyp	Ref	Expression
1		ptuniconst.2	$⊢ J = \prod_{𝑡} (A \times \{R\})$
2		id	$⊢ R \in TopOn (X) \to R \in TopOn (X)$
3	2	ralrimivw	$⊢ R \in TopOn (X) \to \forall x \in A R \in TopOn (X)$
4		fconstmpt	$⊢ A \times \{R\} = (x \in A ⟼ R)$
5	4	fveq2i	$⊢ \prod_{𝑡} (A \times \{R\}) = \prod_{𝑡} ((x \in A ⟼ R))$
6	1 5	eqtri	$⊢ J = \prod_{𝑡} ((x \in A ⟼ R))$
7	6	pttopon	$⊢ (A \in V \land \forall x \in A R \in TopOn (X)) \to J \in TopOn (\underset{x \in A}{⨉} X)$
8	3 7	sylan2	$⊢ (A \in V \land R \in TopOn (X)) \to J \in TopOn (\underset{x \in A}{⨉} X)$
9		toponmax	$⊢ R \in TopOn (X) \to X \in R$
10		ixpconstg	$⊢ (A \in V \land X \in R) \to \underset{x \in A}{⨉} X = X^{A}$
11	9 10	sylan2	$⊢ (A \in V \land R \in TopOn (X)) \to \underset{x \in A}{⨉} X = X^{A}$
12	11	fveq2d	$⊢ (A \in V \land R \in TopOn (X)) \to TopOn (\underset{x \in A}{⨉} X) = TopOn (X^{A})$
13	8 12	eleqtrd	$⊢ (A \in V \land R \in TopOn (X)) \to J \in TopOn (X^{A})$

Metamath Proof Explorer