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