Metamath Proof Explorer

Theorem ptval2

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

Ref Expression
Hypotheses ptval2.1 
|- J = ( Xt_ ` F )
ptval2.2 
|- X = U. J
ptval2.3 
|- G = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
Assertion ptval2 
|- ( ( A e. V /\ F : A --> Top ) -> J = ( topGen ` ( fi ` ( { X } u. ran G ) ) ) )

Proof

Step Hyp Ref Expression
1 ptval2.1 
 |-  J = ( Xt_ ` F )
2 ptval2.2 
 |-  X = U. J
3 ptval2.3 
 |-  G = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
4 ffn 
 |-  ( F : A --> Top -> F Fn A )
5 eqid 
 |-  { 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 ) ) } = { 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 ) ) }
6 5 ptval 
 |-  ( ( A e. V /\ F Fn A ) -> ( Xt_ ` F ) = ( topGen ` { 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 ) ) } ) )
7 1 6 syl5eq 
 |-  ( ( A e. V /\ F Fn A ) -> J = ( topGen ` { 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 ) ) } ) )
8 4 7 sylan2 
 |-  ( ( A e. V /\ F : A --> Top ) -> J = ( topGen ` { 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 ) ) } ) )
9 eqid 
 |-  X_ n e. A U. ( F ` n ) = X_ n e. A U. ( F ` n )
10 5 9 ptbasfi 
 |-  ( ( A e. V /\ F : A --> Top ) -> { 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 ) ) } = ( fi ` ( { X_ n e. A U. ( F ` n ) } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u ) ) ) ) )
11 1 ptuni 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ n e. A U. ( F ` n ) = U. J )
12 11 2 eqtr4di 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ n e. A U. ( F ` n ) = X )
13 12 sneqd 
 |-  ( ( A e. V /\ F : A --> Top ) -> { X_ n e. A U. ( F ` n ) } = { X } )
14 12 3ad2ant1 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ k e. A /\ u e. ( F ` k ) ) -> X_ n e. A U. ( F ` n ) = X )
15 14 mpteq1d 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ k e. A /\ u e. ( F ` k ) ) -> ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) = ( w e. X |-> ( w ` k ) ) )
16 15 cnveqd 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ k e. A /\ u e. ( F ` k ) ) -> `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) = `' ( w e. X |-> ( w ` k ) ) )
17 16 imaeq1d 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ k e. A /\ u e. ( F ` k ) ) -> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u ) = ( `' ( w e. X |-> ( w ` k ) ) " u ) )
18 17 mpoeq3dva 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u ) ) = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) )
19 18 3 eqtr4di 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u ) ) = G )
20 19 rneqd 
 |-  ( ( A e. V /\ F : A --> Top ) -> ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u ) ) = ran G )
21 13 20 uneq12d 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( { X_ n e. A U. ( F ` n ) } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u ) ) ) = ( { X } u. ran G ) )
22 21 fveq2d 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( fi ` ( { X_ n e. A U. ( F ` n ) } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u ) ) ) ) = ( fi ` ( { X } u. ran G ) ) )
23 10 22 eqtrd 
 |-  ( ( A e. V /\ F : A --> Top ) -> { 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 ) ) } = ( fi ` ( { X } u. ran G ) ) )
24 23 fveq2d 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( topGen ` { 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 ) ) } ) = ( topGen ` ( fi ` ( { X } u. ran G ) ) ) )
25 8 24 eqtrd 
 |-  ( ( A e. V /\ F : A --> Top ) -> J = ( topGen ` ( fi ` ( { X } u. ran G ) ) ) )