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 )