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 ) ) )