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 eqtrid
 |-  ( ( 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 )