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 fex 
 |-  ( ( R : I --> TopSp /\ I e. W ) -> R e. _V )
15 4 3 14 syl2anc 
 |-  ( ph -> R e. _V )
16 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
17 4 fdmd 
 |-  ( ph -> dom R = I )
18 eqid 
 |-  ( TopSet ` Y ) = ( TopSet ` Y )
19 1 2 15 16 17 18 prdstset 
 |-  ( ph -> ( TopSet ` Y ) = ( Xt_ ` ( TopOpen o. R ) ) )
20 topnfn 
 |-  TopOpen Fn _V
21 dffn2 
 |-  ( TopOpen Fn _V <-> TopOpen : _V --> _V )
22 20 21 mpbi 
 |-  TopOpen : _V --> _V
23 ssv 
 |-  TopSp C_ _V
24 fss 
 |-  ( ( R : I --> TopSp /\ TopSp C_ _V ) -> R : I --> _V )
25 4 23 24 sylancl 
 |-  ( ph -> R : I --> _V )
26 fcompt 
 |-  ( ( TopOpen : _V --> _V /\ R : I --> _V ) -> ( TopOpen o. R ) = ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) )
27 22 25 26 sylancr 
 |-  ( ph -> ( TopOpen o. R ) = ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) )
28 27 fveq2d 
 |-  ( ph -> ( Xt_ ` ( TopOpen o. R ) ) = ( Xt_ ` ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) ) )
29 19 28 eqtrd 
 |-  ( ph -> ( TopSet ` Y ) = ( Xt_ ` ( x e. I |-> ( TopOpen ` ( R ` x ) ) ) ) )
30 1 2 15 16 17 prdsbas 
 |-  ( ph -> ( Base ` Y ) = X_ x e. I ( Base ` ( R ` x ) ) )
31 30 fveq2d 
 |-  ( ph -> ( TopOn ` ( Base ` Y ) ) = ( TopOn ` X_ x e. I ( Base ` ( R ` x ) ) ) )
32 13 29 31 3eltr4d 
 |-  ( ph -> ( TopSet ` Y ) e. ( TopOn ` ( Base ` Y ) ) )
33 16 18 tsettps 
 |-  ( ( TopSet ` Y ) e. ( TopOn ` ( Base ` Y ) ) -> Y e. TopSp )
34 32 33 syl 
 |-  ( ph -> Y e. TopSp )