Metamath Proof Explorer

Theorem prdstps

Description: A structure product of topological spaces is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses prdstopn.y 
|- Y = ( S Xs_ R )
prdstopn.s 
|- ( ph -> S e. V )
prdstopn.i 
|- ( ph -> I e. W )
prdstps.r 
|- ( ph -> R : I --> TopSp )
Assertion prdstps 
|- ( ph -> Y e. TopSp )

Proof

Step Hyp Ref Expression
1 prdstopn.y 
 |-  Y = ( S Xs_ R )
2 prdstopn.s 
 |-  ( ph -> S e. V )
3 prdstopn.i 
 |-  ( ph -> I e. W )
4 prdstps.r 
 |-  ( ph -> R : I --> TopSp )
5 4 ffvelrnda 
 |-  ( ( ph /\ x e. I ) -> ( R ` x ) e. TopSp )
6 eqid 
 |-  ( Base ` ( R ` x ) ) = ( Base ` ( R ` x ) )
7 eqid 
 |-  ( TopOpen ` ( R ` x ) ) = ( TopOpen ` ( R ` x ) )
8 6 7 istps 
 |-  ( ( R ` x ) e. TopSp <-> ( TopOpen ` ( R ` x ) ) e. ( TopOn ` ( Base ` ( R ` x ) ) ) )
9 5 8 sylib 
 |-  ( ( ph /\ x e. I ) -> ( TopOpen ` ( R ` x ) ) e. ( TopOn ` ( Base ` ( R ` x ) ) ) )
10 9 ralrimiva 
 |-  ( ph -> A. x e. I ( TopOpen ` ( R ` x ) ) e. ( TopOn ` ( Base ` ( R ` x ) ) ) )
11 eqid 
 |-  ( Xt_ ` ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) ) = ( Xt_ ` ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) )
12 11 pttopon 
 |-  ( ( I e. W /\ A. x e. I ( TopOpen ` ( R ` x ) ) e. ( TopOn ` ( Base ` ( R ` x ) ) ) ) -> ( Xt_ ` ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) ) e. ( TopOn ` X_ x e. I ( Base ` ( R ` x ) ) ) )
13 3 10 12 syl2anc 
 |-  ( ph -> ( Xt_ ` ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) ) e. ( TopOn ` X_ x e. I ( Base ` ( R ` x ) ) ) )
14 4 3 fexd 
 |-  ( ph -> R e. _V )
15 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
16 4 fdmd 
 |-  ( ph -> dom R = I )
17 eqid 
 |-  ( TopSet ` Y ) = ( TopSet ` Y )
18 1 2 14 15 16 17 prdstset 
 |-  ( ph -> ( TopSet ` Y ) = ( Xt_ ` ( TopOpen o. R ) ) )
19 topnfn 
 |-  TopOpen Fn _V
20 dffn2 
 |-  ( TopOpen Fn _V <-> TopOpen : _V --> _V )
21 19 20 mpbi 
 |-  TopOpen : _V --> _V
22 ssv 
 |-  TopSp C_ _V
23 fss 
 |-  ( ( R : I --> TopSp /\ TopSp C_ _V ) -> R : I --> _V )
24 4 22 23 sylancl 
 |-  ( ph -> R : I --> _V )
25 fcompt 
 |-  ( ( TopOpen : _V --> _V /\ R : I --> _V ) -> ( TopOpen o. R ) = ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) )
26 21 24 25 sylancr 
 |-  ( ph -> ( TopOpen o. R ) = ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) )
27 26 fveq2d 
 |-  ( ph -> ( Xt_ ` ( TopOpen o. R ) ) = ( Xt_ ` ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) ) )
28 18 27 eqtrd 
 |-  ( ph -> ( TopSet ` Y ) = ( Xt_ ` ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) ) )
29 1 2 14 15 16 prdsbas 
 |-  ( ph -> ( Base ` Y ) = X_ x e. I ( Base ` ( R ` x ) ) )
30 29 fveq2d 
 |-  ( ph -> ( TopOn ` ( Base ` Y ) ) = ( TopOn ` X_ x e. I ( Base ` ( R ` x ) ) ) )
31 13 28 30 3eltr4d 
 |-  ( ph -> ( TopSet ` Y ) e. ( TopOn ` ( Base ` Y ) ) )
32 15 17 tsettps 
 |-  ( ( TopSet ` Y ) e. ( TopOn ` ( Base ` Y ) ) -> Y e. TopSp )
33 31 32 syl 
 |-  ( ph -> Y e. TopSp )