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

Metamath Proof Explorer

Theorem ptuni2

Description: The base set for the product topology. (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 ptuni2 
|- ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. 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 ptbasid 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) e. B )
3 elssuni 
 |-  ( X_ k e. A U. ( F ` k ) e. B -> X_ k e. A U. ( F ` k ) C_ U. B )
4 2 3 syl 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) C_ U. B )
5 simpr2 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( 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 ) ) ) -> A. y e. A ( g ` y ) e. ( F ` y ) )
6 elssuni 
 |-  ( ( g ` y ) e. ( F ` y ) -> ( g ` y ) C_ U. ( F ` y ) )
7 6 ralimi 
 |-  ( A. y e. A ( g ` y ) e. ( F ` y ) -> A. y e. A ( g ` y ) C_ U. ( F ` y ) )
8 ss2ixp 
 |-  ( A. y e. A ( g ` y ) C_ U. ( F ` y ) -> X_ y e. A ( g ` y ) C_ X_ y e. A U. ( F ` y ) )
9 5 7 8 3syl 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( 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_ y e. A ( g ` y ) C_ X_ y e. A U. ( F ` y ) )
10 fveq2 
 |-  ( y = k -> ( F ` y ) = ( F ` k ) )
11 10 unieqd 
 |-  ( y = k -> U. ( F ` y ) = U. ( F ` k ) )
12 11 cbvixpv 
 |-  X_ y e. A U. ( F ` y ) = X_ k e. A U. ( F ` k )
13 9 12 sseqtrdi 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( 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_ y e. A ( g ` y ) C_ X_ k e. A U. ( F ` k ) )
14 velpw 
 |-  ( x e. ~P X_ k e. A U. ( F ` k ) <-> x C_ X_ k e. A U. ( F ` k ) )
15 sseq1 
 |-  ( x = X_ y e. A ( g ` y ) -> ( x C_ X_ k e. A U. ( F ` k ) <-> X_ y e. A ( g ` y ) C_ X_ k e. A U. ( F ` k ) ) )
16 14 15 bitrid 
 |-  ( x = X_ y e. A ( g ` y ) -> ( x e. ~P X_ k e. A U. ( F ` k ) <-> X_ y e. A ( g ` y ) C_ X_ k e. A U. ( F ` k ) ) )
17 13 16 syl5ibrcom 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( 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 ) -> x e. ~P X_ k e. A U. ( F ` k ) ) )
18 17 expimpd 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( ( ( 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 ) ) -> x e. ~P X_ k e. A U. ( F ` k ) ) )
19 18 exlimdv 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( 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 ) ) -> x e. ~P X_ k e. A U. ( F ` k ) ) )
20 19 abssdv 
 |-  ( ( A e. V /\ F : A --> Top ) -> { 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 ) ) } C_ ~P X_ k e. A U. ( F ` k ) )
21 1 20 eqsstrid 
 |-  ( ( A e. V /\ F : A --> Top ) -> B C_ ~P X_ k e. A U. ( F ` k ) )
22 sspwuni 
 |-  ( B C_ ~P X_ k e. A U. ( F ` k ) <-> U. B C_ X_ k e. A U. ( F ` k ) )
23 21 22 sylib 
 |-  ( ( A e. V /\ F : A --> Top ) -> U. B C_ X_ k e. A U. ( F ` k ) )
24 4 23 eqssd 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. B )