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=𝑡A×R
ptuniconst.1 X=R
Assertion ptuniconst AVRTopXA=J

Proof

Step Hyp Ref Expression
1 ptuniconst.2 J=𝑡A×R
2 ptuniconst.1 X=R
3 2 toptopon RTopRTopOnX
4 1 pttoponconst AVRTopOnXJTopOnXA
5 3 4 sylan2b AVRTopJTopOnXA
6 toponuni JTopOnXAXA=J
7 5 6 syl AVRTopXA=J