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 = ( Xt_ ` ( A X. { R } ) )
	ptuniconst.1	|- X = U. R
Assertion	ptuniconst	|- ( ( A e. V /\ R e. Top ) -> ( X ^m A ) = U. J )

Proof

Step	Hyp	Ref	Expression
1		ptuniconst.2	|- J = ( Xt_ ` ( A X. { R } ) )
2		ptuniconst.1	|- X = U. R
3	2	toptopon	|- ( R e. Top <-> R e. ( TopOn ` X ) )
4	1	pttoponconst	|- ( ( A e. V /\ R e. ( TopOn ` X ) ) -> J e. ( TopOn ` ( X ^m A ) ) )
5	3 4	sylan2b	|- ( ( A e. V /\ R e. Top ) -> J e. ( TopOn ` ( X ^m A ) ) )
6		toponuni	|- ( J e. ( TopOn ` ( X ^m A ) ) -> ( X ^m A ) = U. J )
7	5 6	syl	|- ( ( A e. V /\ R e. Top ) -> ( X ^m A ) = U. J )