Metamath Proof Explorer

Theorem prdstopn

Description: Topology of a structure product. (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 )
prdstopn.r 
|- ( ph -> R Fn I )
prdstopn.o 
|- O = ( TopOpen ` Y )
Assertion prdstopn 
|- ( ph -> O = ( Xt_ ` ( TopOpen o. R ) ) )

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 prdstopn.r 
 |-  ( ph -> R Fn I )
5 prdstopn.o 
 |-  O = ( TopOpen ` Y )
6 fnex 
 |-  ( ( R Fn I /\ I e. W ) -> R e. _V )
7 4 3 6 syl2anc 
 |-  ( ph -> R e. _V )
8 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
9 eqidd 
 |-  ( ph -> dom R = dom R )
10 eqid 
 |-  ( TopSet ` Y ) = ( TopSet ` Y )
11 1 2 7 8 9 10 prdstset 
 |-  ( ph -> ( TopSet ` Y ) = ( Xt_ ` ( TopOpen o. R ) ) )
12 topnfn 
 |-  TopOpen Fn _V
13 dffn2 
 |-  ( R Fn I <-> R : I --> _V )
14 4 13 sylib 
 |-  ( ph -> R : I --> _V )
15 fnfco 
 |-  ( ( TopOpen Fn _V /\ R : I --> _V ) -> ( TopOpen o. R ) Fn I )
16 12 14 15 sylancr 
 |-  ( ph -> ( TopOpen o. R ) Fn I )
17 eqid 
 |-  { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } = { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) }
18 17 ptval 
 |-  ( ( I e. W /\ ( TopOpen o. R ) Fn I ) -> ( Xt_ ` ( TopOpen o. R ) ) = ( topGen ` { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } ) )
19 3 16 18 syl2anc 
 |-  ( ph -> ( Xt_ ` ( TopOpen o. R ) ) = ( topGen ` { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } ) )
20 19 unieqd 
 |-  ( ph -> U. ( Xt_ ` ( TopOpen o. R ) ) = U. ( topGen ` { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } ) )
21 fvco2 
 |-  ( ( R Fn I /\ y e. I ) -> ( ( TopOpen o. R ) ` y ) = ( TopOpen ` ( R ` y ) ) )
22 4 21 sylan 
 |-  ( ( ph /\ y e. I ) -> ( ( TopOpen o. R ) ` y ) = ( TopOpen ` ( R ` y ) ) )
23 eqid 
 |-  ( Base ` ( R ` y ) ) = ( Base ` ( R ` y ) )
24 eqid 
 |-  ( TopSet ` ( R ` y ) ) = ( TopSet ` ( R ` y ) )
25 23 24 topnval 
 |-  ( ( TopSet ` ( R ` y ) ) |`t ( Base ` ( R ` y ) ) ) = ( TopOpen ` ( R ` y ) )
26 restsspw 
 |-  ( ( TopSet ` ( R ` y ) ) |`t ( Base ` ( R ` y ) ) ) C_ ~P ( Base ` ( R ` y ) )
27 25 26 eqsstrri 
 |-  ( TopOpen ` ( R ` y ) ) C_ ~P ( Base ` ( R ` y ) )
28 22 27 eqsstrdi 
 |-  ( ( ph /\ y e. I ) -> ( ( TopOpen o. R ) ` y ) C_ ~P ( Base ` ( R ` y ) ) )
29 28 sseld 
 |-  ( ( ph /\ y e. I ) -> ( ( g ` y ) e. ( ( TopOpen o. R ) ` y ) -> ( g ` y ) e. ~P ( Base ` ( R ` y ) ) ) )
30 fvex 
 |-  ( g ` y ) e. _V
31 30 elpw 
 |-  ( ( g ` y ) e. ~P ( Base ` ( R ` y ) ) <-> ( g ` y ) C_ ( Base ` ( R ` y ) ) )
32 29 31 imbitrdi 
 |-  ( ( ph /\ y e. I ) -> ( ( g ` y ) e. ( ( TopOpen o. R ) ` y ) -> ( g ` y ) C_ ( Base ` ( R ` y ) ) ) )
33 32 ralimdva 
 |-  ( ph -> ( A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) -> A. y e. I ( g ` y ) C_ ( Base ` ( R ` y ) ) ) )
34 simpl2 
 |-  ( ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) -> A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) )
35 33 34 impel 
 |-  ( ( ph /\ ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) ) -> A. y e. I ( g ` y ) C_ ( Base ` ( R ` y ) ) )
36 ss2ixp 
 |-  ( A. y e. I ( g ` y ) C_ ( Base ` ( R ` y ) ) -> X_ y e. I ( g ` y ) C_ X_ y e. I ( Base ` ( R ` y ) ) )
37 35 36 syl 
 |-  ( ( ph /\ ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) ) -> X_ y e. I ( g ` y ) C_ X_ y e. I ( Base ` ( R ` y ) ) )
38 simprr 
 |-  ( ( ph /\ ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) ) -> x = X_ y e. I ( g ` y ) )
39 1 8 2 3 4 prdsbas2 
 |-  ( ph -> ( Base ` Y ) = X_ y e. I ( Base ` ( R ` y ) ) )
40 39 adantr 
 |-  ( ( ph /\ ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) ) -> ( Base ` Y ) = X_ y e. I ( Base ` ( R ` y ) ) )
41 37 38 40 3sstr4d 
 |-  ( ( ph /\ ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) ) -> x C_ ( Base ` Y ) )
42 41 ex 
 |-  ( ph -> ( ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) -> x C_ ( Base ` Y ) ) )
43 42 exlimdv 
 |-  ( ph -> ( E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) -> x C_ ( Base ` Y ) ) )
44 velpw 
 |-  ( x e. ~P ( Base ` Y ) <-> x C_ ( Base ` Y ) )
45 43 44 imbitrrdi 
 |-  ( ph -> ( E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) -> x e. ~P ( Base ` Y ) ) )
46 45 abssdv 
 |-  ( ph -> { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } C_ ~P ( Base ` Y ) )
47 fvex 
 |-  ( Base ` Y ) e. _V
48 47 pwex 
 |-  ~P ( Base ` Y ) e. _V
49 48 ssex 
 |-  ( { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } C_ ~P ( Base ` Y ) -> { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } e. _V )
50 unitg 
 |-  ( { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } e. _V -> U. ( topGen ` { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } ) = U. { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } )
51 46 49 50 3syl 
 |-  ( ph -> U. ( topGen ` { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } ) = U. { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } )
52 20 51 eqtrd 
 |-  ( ph -> U. ( Xt_ ` ( TopOpen o. R ) ) = U. { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } )
53 sspwuni 
 |-  ( { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } C_ ~P ( Base ` Y ) <-> U. { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } C_ ( Base ` Y ) )
54 46 53 sylib 
 |-  ( ph -> U. { x | E. g ( ( g Fn I /\ A. y e. I ( g ` y ) e. ( ( TopOpen o. R ) ` y ) /\ E. z e. Fin A. y e. ( I \ z ) ( g ` y ) = U. ( ( TopOpen o. R ) ` y ) ) /\ x = X_ y e. I ( g ` y ) ) } C_ ( Base ` Y ) )
55 52 54 eqsstrd 
 |-  ( ph -> U. ( Xt_ ` ( TopOpen o. R ) ) C_ ( Base ` Y ) )
56 sspwuni 
 |-  ( ( Xt_ ` ( TopOpen o. R ) ) C_ ~P ( Base ` Y ) <-> U. ( Xt_ ` ( TopOpen o. R ) ) C_ ( Base ` Y ) )
57 55 56 sylibr 
 |-  ( ph -> ( Xt_ ` ( TopOpen o. R ) ) C_ ~P ( Base ` Y ) )
58 11 57 eqsstrd 
 |-  ( ph -> ( TopSet ` Y ) C_ ~P ( Base ` Y ) )
59 8 10 topnid 
 |-  ( ( TopSet ` Y ) C_ ~P ( Base ` Y ) -> ( TopSet ` Y ) = ( TopOpen ` Y ) )
60 58 59 syl 
 |-  ( ph -> ( TopSet ` Y ) = ( TopOpen ` Y ) )
61 60 5 eqtr4di 
 |-  ( ph -> ( TopSet ` Y ) = O )
62 61 11 eqtr3d 
 |-  ( ph -> O = ( Xt_ ` ( TopOpen o. R ) ) )