# 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 )`
` |-  ( ( ( A e. V /\ F : A --> Top ) /\ k e. A ) -> ( F ` k ) e. Top )`
` |-  U. ( F ` k ) = U. ( F ` k )`
` |-  ( ( F ` k ) e. Top -> U. ( F ` k ) e. ( F ` k ) )`
` |-  ( ( ( A e. V /\ F : A --> Top ) /\ k e. A ) -> U. ( F ` k ) e. ( F ` k ) )`
` |-  ( ( ( A e. V /\ F : A --> Top ) /\ k e. ( A \ (/) ) ) -> U. ( F ` k ) = U. ( F ` k ) )`
` |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) e. B )`