Metamath Proof Explorer


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 )