# 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 syl5eq
` |-  ( 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 )`