Theorem ptuniconst

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

	Ref	Expression
Hypotheses	ptuniconst.2	$$⊢J={\prod }_{𝑡}\left(A\times \left\{R\right\}\right)$$
	ptuniconst.1	$$⊢X=\bigcup R$$
Assertion	ptuniconst	$$⊢\left(A\in V\wedge R\in \mathrm{Top}\right)\to X^A=\bigcup J$$

Proof

Step	Hyp	Ref	Expression
1		ptuniconst.2	$$⊢J={\prod }_{𝑡}\left(A\times \left\{R\right\}\right)$$
2		ptuniconst.1	$$⊢X=\bigcup R$$
3	2	toptopon	$$⊢R\in \mathrm{Top}\leftrightarrow R\in \mathrm{TopOn}\left(X\right)$$
4	1	pttoponconst	$$⊢\left(A\in V\wedge R\in \mathrm{TopOn}\left(X\right)\right)\to J\in \mathrm{TopOn}\left(X^A\right)$$
5	3 4	sylan2b	$$⊢\left(A\in V\wedge R\in \mathrm{Top}\right)\to J\in \mathrm{TopOn}\left(X^A\right)$$
6		toponuni	$$⊢J\in \mathrm{TopOn}\left(X^A\right)\to X^A=\bigcup J$$
7	5 6	syl	$$⊢\left(A\in V\wedge R\in \mathrm{Top}\right)\to X^A=\bigcup J$$