Metamath Proof Explorer

Theorem ptval

Description: The value of the product topology function. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypothesis ptval.1 
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }
Assertion ptval 
|- ( ( A e. V /\ F Fn A ) -> ( Xt_ ` F ) = ( topGen ` B ) )

Proof

Step Hyp Ref Expression
1 ptval.1 
 |-  B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }
2 df-pt 
 |-  Xt_ = ( f e. _V |-> ( topGen ` { x | E. g ( ( g Fn dom f /\ A. y e. dom f ( g ` y ) e. ( f ` y ) /\ E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) ) /\ x = X_ y e. dom f ( g ` y ) ) } ) )
3 simpr 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> f = F )
4 3 dmeqd 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> dom f = dom F )
5 fndm 
 |-  ( F Fn A -> dom F = A )
6 5 ad2antlr 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> dom F = A )
7 4 6 eqtrd 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> dom f = A )
8 7 fneq2d 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( g Fn dom f <-> g Fn A ) )
9 3 fveq1d 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( f ` y ) = ( F ` y ) )
10 9 eleq2d 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( ( g ` y ) e. ( f ` y ) <-> ( g ` y ) e. ( F ` y ) ) )
11 7 10 raleqbidv 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( A. y e. dom f ( g ` y ) e. ( f ` y ) <-> A. y e. A ( g ` y ) e. ( F ` y ) ) )
12 7 difeq1d 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( dom f \ z ) = ( A \ z ) )
13 9 unieqd 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> U. ( f ` y ) = U. ( F ` y ) )
14 13 eqeq2d 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( ( g ` y ) = U. ( f ` y ) <-> ( g ` y ) = U. ( F ` y ) ) )
15 12 14 raleqbidv 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) <-> A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) )
16 15 rexbidv 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) <-> E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) )
17 8 11 16 3anbi123d 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( ( g Fn dom f /\ A. y e. dom f ( g ` y ) e. ( f ` y ) /\ E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) ) <-> ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) )
18 7 ixpeq1d 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> X_ y e. dom f ( g ` y ) = X_ y e. A ( g ` y ) )
19 18 eqeq2d 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( x = X_ y e. dom f ( g ` y ) <-> x = X_ y e. A ( g ` y ) ) )
20 17 19 anbi12d 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( ( ( g Fn dom f /\ A. y e. dom f ( g ` y ) e. ( f ` y ) /\ E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) ) /\ x = X_ y e. dom f ( g ` y ) ) <-> ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) ) )
21 20 exbidv 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( E. g ( ( g Fn dom f /\ A. y e. dom f ( g ` y ) e. ( f ` y ) /\ E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) ) /\ x = X_ y e. dom f ( g ` y ) ) <-> E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) ) )
22 21 abbidv 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> { x | E. g ( ( g Fn dom f /\ A. y e. dom f ( g ` y ) e. ( f ` y ) /\ E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) ) /\ x = X_ y e. dom f ( g ` y ) ) } = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } )
23 22 1 eqtr4di 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> { x | E. g ( ( g Fn dom f /\ A. y e. dom f ( g ` y ) e. ( f ` y ) /\ E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) ) /\ x = X_ y e. dom f ( g ` y ) ) } = B )
24 23 fveq2d 
 |-  ( ( ( A e. V /\ F Fn A ) /\ f = F ) -> ( topGen ` { x | E. g ( ( g Fn dom f /\ A. y e. dom f ( g ` y ) e. ( f ` y ) /\ E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) ) /\ x = X_ y e. dom f ( g ` y ) ) } ) = ( topGen ` B ) )
25 fnex 
 |-  ( ( F Fn A /\ A e. V ) -> F e. _V )
26 25 ancoms 
 |-  ( ( A e. V /\ F Fn A ) -> F e. _V )
27 fvexd 
 |-  ( ( A e. V /\ F Fn A ) -> ( topGen ` B ) e. _V )
28 2 24 26 27 fvmptd2 
 |-  ( ( A e. V /\ F Fn A ) -> ( Xt_ ` F ) = ( topGen ` B ) )