Metamath Proof Explorer


Theorem 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 = ( Xt_ ` ( A X. { R } ) )
Assertion pttoponconst
|- ( ( A e. V /\ R e. ( TopOn ` X ) ) -> J e. ( TopOn ` ( X ^m A ) ) )

Proof

Step Hyp Ref Expression
1 ptuniconst.2
 |-  J = ( Xt_ ` ( A X. { R } ) )
2 id
 |-  ( R e. ( TopOn ` X ) -> R e. ( TopOn ` X ) )
3 2 ralrimivw
 |-  ( R e. ( TopOn ` X ) -> A. x e. A R e. ( TopOn ` X ) )
4 fconstmpt
 |-  ( A X. { R } ) = ( x e. A |-> R )
5 4 fveq2i
 |-  ( Xt_ ` ( A X. { R } ) ) = ( Xt_ ` ( x e. A |-> R ) )
6 1 5 eqtri
 |-  J = ( Xt_ ` ( x e. A |-> R ) )
7 6 pttopon
 |-  ( ( A e. V /\ A. x e. A R e. ( TopOn ` X ) ) -> J e. ( TopOn ` X_ x e. A X ) )
8 3 7 sylan2
 |-  ( ( A e. V /\ R e. ( TopOn ` X ) ) -> J e. ( TopOn ` X_ x e. A X ) )
9 toponmax
 |-  ( R e. ( TopOn ` X ) -> X e. R )
10 ixpconstg
 |-  ( ( A e. V /\ X e. R ) -> X_ x e. A X = ( X ^m A ) )
11 9 10 sylan2
 |-  ( ( A e. V /\ R e. ( TopOn ` X ) ) -> X_ x e. A X = ( X ^m A ) )
12 11 fveq2d
 |-  ( ( A e. V /\ R e. ( TopOn ` X ) ) -> ( TopOn ` X_ x e. A X ) = ( TopOn ` ( X ^m A ) ) )
13 8 12 eleqtrd
 |-  ( ( A e. V /\ R e. ( TopOn ` X ) ) -> J e. ( TopOn ` ( X ^m A ) ) )