This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ptbasin2

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-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 ptbasin2 
|- ( ( A e. V /\ F : A --> Top ) -> ( fi ` B ) = 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 1 ptbasin 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( u e. B /\ v e. B ) ) -> ( u i^i v ) e. B )
3 2 ralrimivva 
 |-  ( ( A e. V /\ F : A --> Top ) -> A. u e. B A. v e. B ( u i^i v ) e. B )
4 1 ptuni2 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. B )
5 ixpexg 
 |-  ( A. k e. A U. ( F ` k ) e. _V -> X_ k e. A U. ( F ` k ) e. _V )
6 fvex 
 |-  ( F ` k ) e. _V
7 6 uniex 
 |-  U. ( F ` k ) e. _V
8 7 a1i 
 |-  ( k e. A -> U. ( F ` k ) e. _V )
9 5 8 mprg 
 |-  X_ k e. A U. ( F ` k ) e. _V
10 4 9 eqeltrrdi 
 |-  ( ( A e. V /\ F : A --> Top ) -> U. B e. _V )
11 uniexb 
 |-  ( B e. _V <-> U. B e. _V )
12 10 11 sylibr 
 |-  ( ( A e. V /\ F : A --> Top ) -> B e. _V )
13 inficl 
 |-  ( B e. _V -> ( A. u e. B A. v e. B ( u i^i v ) e. B <-> ( fi ` B ) = B ) )
14 12 13 syl 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( A. u e. B A. v e. B ( u i^i v ) e. B <-> ( fi ` B ) = B ) )
15 3 14 mpbid 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( fi ` B ) = B )