Metamath Proof Explorer


Theorem ptbasid

Description: The base set of the product topology is a basic open set. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypothesis ptbas.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 ptbasid
|- ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) e. B )

Proof

Step Hyp Ref Expression
1 ptbas.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 simpl
 |-  ( ( A e. V /\ F : A --> Top ) -> A e. V )
3 0fin
 |-  (/) e. Fin
4 3 a1i
 |-  ( ( A e. V /\ F : A --> Top ) -> (/) e. Fin )
5 ffvelrn
 |-  ( ( F : A --> Top /\ k e. A ) -> ( F ` k ) e. Top )
6 5 adantll
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ k e. A ) -> ( F ` k ) e. Top )
7 eqid
 |-  U. ( F ` k ) = U. ( F ` k )
8 7 topopn
 |-  ( ( F ` k ) e. Top -> U. ( F ` k ) e. ( F ` k ) )
9 6 8 syl
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ k e. A ) -> U. ( F ` k ) e. ( F ` k ) )
10 eqidd
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ k e. ( A \ (/) ) ) -> U. ( F ` k ) = U. ( F ` k ) )
11 1 2 4 9 10 elptr2
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) e. B )