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

Metamath Proof Explorer

Theorem elptr2

Description: A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypotheses 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 ) ) }
elptr2.1 
|- ( ph -> A e. V )
elptr2.2 
|- ( ph -> W e. Fin )
elptr2.3 
|- ( ( ph /\ k e. A ) -> S e. ( F ` k ) )
elptr2.4 
|- ( ( ph /\ k e. ( A \ W ) ) -> S = U. ( F ` k ) )
Assertion elptr2 
|- ( ph -> X_ k e. A S 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 elptr2.1 
 |-  ( ph -> A e. V )
3 elptr2.2 
 |-  ( ph -> W e. Fin )
4 elptr2.3 
 |-  ( ( ph /\ k e. A ) -> S e. ( F ` k ) )
5 elptr2.4 
 |-  ( ( ph /\ k e. ( A \ W ) ) -> S = U. ( F ` k ) )
6 nffvmpt1 
 |-  F/_ k ( ( k e. A |-> S ) ` y )
7 nfcv 
 |-  F/_ y ( ( k e. A |-> S ) ` k )
8 fveq2 
 |-  ( y = k -> ( ( k e. A |-> S ) ` y ) = ( ( k e. A |-> S ) ` k ) )
9 6 7 8 cbvixp 
 |-  X_ y e. A ( ( k e. A |-> S ) ` y ) = X_ k e. A ( ( k e. A |-> S ) ` k )
10 simpr 
 |-  ( ( ph /\ k e. A ) -> k e. A )
11 eqid 
 |-  ( k e. A |-> S ) = ( k e. A |-> S )
12 11 fvmpt2 
 |-  ( ( k e. A /\ S e. ( F ` k ) ) -> ( ( k e. A |-> S ) ` k ) = S )
13 10 4 12 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> S ) ` k ) = S )
14 13 ixpeq2dva 
 |-  ( ph -> X_ k e. A ( ( k e. A |-> S ) ` k ) = X_ k e. A S )
15 9 14 eqtrid 
 |-  ( ph -> X_ y e. A ( ( k e. A |-> S ) ` y ) = X_ k e. A S )
16 4 ralrimiva 
 |-  ( ph -> A. k e. A S e. ( F ` k ) )
17 11 fnmpt 
 |-  ( A. k e. A S e. ( F ` k ) -> ( k e. A |-> S ) Fn A )
18 16 17 syl 
 |-  ( ph -> ( k e. A |-> S ) Fn A )
19 13 4 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> S ) ` k ) e. ( F ` k ) )
20 19 ralrimiva 
 |-  ( ph -> A. k e. A ( ( k e. A |-> S ) ` k ) e. ( F ` k ) )
21 6 nfel1 
 |-  F/ k ( ( k e. A |-> S ) ` y ) e. ( F ` y )
22 nfv 
 |-  F/ y ( ( k e. A |-> S ) ` k ) e. ( F ` k )
23 fveq2 
 |-  ( y = k -> ( F ` y ) = ( F ` k ) )
24 8 23 eleq12d 
 |-  ( y = k -> ( ( ( k e. A |-> S ) ` y ) e. ( F ` y ) <-> ( ( k e. A |-> S ) ` k ) e. ( F ` k ) ) )
25 21 22 24 cbvralw 
 |-  ( A. y e. A ( ( k e. A |-> S ) ` y ) e. ( F ` y ) <-> A. k e. A ( ( k e. A |-> S ) ` k ) e. ( F ` k ) )
26 20 25 sylibr 
 |-  ( ph -> A. y e. A ( ( k e. A |-> S ) ` y ) e. ( F ` y ) )
27 eldifi 
 |-  ( k e. ( A \ W ) -> k e. A )
28 27 13 sylan2 
 |-  ( ( ph /\ k e. ( A \ W ) ) -> ( ( k e. A |-> S ) ` k ) = S )
29 28 5 eqtrd 
 |-  ( ( ph /\ k e. ( A \ W ) ) -> ( ( k e. A |-> S ) ` k ) = U. ( F ` k ) )
30 29 ralrimiva 
 |-  ( ph -> A. k e. ( A \ W ) ( ( k e. A |-> S ) ` k ) = U. ( F ` k ) )
31 6 nfeq1 
 |-  F/ k ( ( k e. A |-> S ) ` y ) = U. ( F ` y )
32 nfv 
 |-  F/ y ( ( k e. A |-> S ) ` k ) = U. ( F ` k )
33 23 unieqd 
 |-  ( y = k -> U. ( F ` y ) = U. ( F ` k ) )
34 8 33 eqeq12d 
 |-  ( y = k -> ( ( ( k e. A |-> S ) ` y ) = U. ( F ` y ) <-> ( ( k e. A |-> S ) ` k ) = U. ( F ` k ) ) )
35 31 32 34 cbvralw 
 |-  ( A. y e. ( A \ W ) ( ( k e. A |-> S ) ` y ) = U. ( F ` y ) <-> A. k e. ( A \ W ) ( ( k e. A |-> S ) ` k ) = U. ( F ` k ) )
36 30 35 sylibr 
 |-  ( ph -> A. y e. ( A \ W ) ( ( k e. A |-> S ) ` y ) = U. ( F ` y ) )
37 1 elptr 
 |-  ( ( A e. V /\ ( ( k e. A |-> S ) Fn A /\ A. y e. A ( ( k e. A |-> S ) ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( ( k e. A |-> S ) ` y ) = U. ( F ` y ) ) ) -> X_ y e. A ( ( k e. A |-> S ) ` y ) e. B )
38 2 18 26 3 36 37 syl122anc 
 |-  ( ph -> X_ y e. A ( ( k e. A |-> S ) ` y ) e. B )
39 15 38 eqeltrrd 
 |-  ( ph -> X_ k e. A S e. B )