Metamath Proof Explorer

Theorem ptuni

Description: The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypothesis ptuni.1 
|- J = ( Xt_ ` F )
Assertion ptuni 
|- ( ( A e. V /\ F : A --> Top ) -> X_ x e. A U. ( F ` x ) = U. J )

Proof

Step Hyp Ref Expression
1 ptuni.1 
 |-  J = ( Xt_ ` F )
2 eqid 
 |-  { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } = { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) }
3 2 ptbas 
 |-  ( ( A e. V /\ F : A --> Top ) -> { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } e. TopBases )
4 unitg 
 |-  ( { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } e. TopBases -> U. ( topGen ` { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } ) = U. { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } )
5 3 4 syl 
 |-  ( ( A e. V /\ F : A --> Top ) -> U. ( topGen ` { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } ) = U. { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } )
6 ffn 
 |-  ( F : A --> Top -> F Fn A )
7 2 ptval 
 |-  ( ( A e. V /\ F Fn A ) -> ( Xt_ ` F ) = ( topGen ` { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } ) )
8 6 7 sylan2 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) = ( topGen ` { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } ) )
9 1 8 syl5eq 
 |-  ( ( A e. V /\ F : A --> Top ) -> J = ( topGen ` { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } ) )
10 9 unieqd 
 |-  ( ( A e. V /\ F : A --> Top ) -> U. J = U. ( topGen ` { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } ) )
11 2 ptuni2 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ x e. A U. ( F ` x ) = U. { k | 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 ) ) /\ k = X_ y e. A ( g ` y ) ) } )
12 5 10 11 3eqtr4rd 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ x e. A U. ( F ` x ) = U. J )