Metamath Proof Explorer

Theorem elpt

Description: Elementhood in the bases of a 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 elpt 
|- ( S e. B <-> E. h ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. w e. Fin A. y e. ( A \ w ) ( h ` y ) = U. ( F ` y ) ) /\ S = X_ y e. A ( h ` y ) ) )

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 eleq2i 
 |-  ( S e. B <-> S e. { 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 ) ) } )
3 simpr 
 |-  ( ( ( 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 ) ) /\ S = X_ y e. A ( g ` y ) ) -> S = X_ y e. A ( g ` y ) )
4 ixpexg 
 |-  ( A. y e. A ( g ` y ) e. _V -> X_ y e. A ( g ` y ) e. _V )
5 fvexd 
 |-  ( y e. A -> ( g ` y ) e. _V )
6 4 5 mprg 
 |-  X_ y e. A ( g ` y ) e. _V
7 3 6 eqeltrdi 
 |-  ( ( ( 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 ) ) /\ S = X_ y e. A ( g ` y ) ) -> S e. _V )
8 7 exlimiv 
 |-  ( 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 ) ) /\ S = X_ y e. A ( g ` y ) ) -> S e. _V )
9 eqeq1 
 |-  ( x = S -> ( x = X_ y e. A ( g ` y ) <-> S = X_ y e. A ( g ` y ) ) )
10 9 anbi2d 
 |-  ( x = S -> ( ( ( 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 ) ) <-> ( ( 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 ) ) /\ S = X_ y e. A ( g ` y ) ) ) )
11 10 exbidv 
 |-  ( x = S -> ( 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 ) ) <-> 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 ) ) /\ S = X_ y e. A ( g ` y ) ) ) )
12 8 11 elab3 
 |-  ( S e. { 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 ) ) } <-> 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 ) ) /\ S = X_ y e. A ( g ` y ) ) )
13 fneq1 
 |-  ( g = h -> ( g Fn A <-> h Fn A ) )
14 fveq1 
 |-  ( g = h -> ( g ` y ) = ( h ` y ) )
15 14 eleq1d 
 |-  ( g = h -> ( ( g ` y ) e. ( F ` y ) <-> ( h ` y ) e. ( F ` y ) ) )
16 15 ralbidv 
 |-  ( g = h -> ( A. y e. A ( g ` y ) e. ( F ` y ) <-> A. y e. A ( h ` y ) e. ( F ` y ) ) )
17 14 eqeq1d 
 |-  ( g = h -> ( ( g ` y ) = U. ( F ` y ) <-> ( h ` y ) = U. ( F ` y ) ) )
18 17 rexralbidv 
 |-  ( g = h -> ( E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) <-> E. z e. Fin A. y e. ( A \ z ) ( h ` y ) = U. ( F ` y ) ) )
19 difeq2 
 |-  ( z = w -> ( A \ z ) = ( A \ w ) )
20 19 raleqdv 
 |-  ( z = w -> ( A. y e. ( A \ z ) ( h ` y ) = U. ( F ` y ) <-> A. y e. ( A \ w ) ( h ` y ) = U. ( F ` y ) ) )
21 20 cbvrexvw 
 |-  ( E. z e. Fin A. y e. ( A \ z ) ( h ` y ) = U. ( F ` y ) <-> E. w e. Fin A. y e. ( A \ w ) ( h ` y ) = U. ( F ` y ) )
22 18 21 bitrdi 
 |-  ( g = h -> ( E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) <-> E. w e. Fin A. y e. ( A \ w ) ( h ` y ) = U. ( F ` y ) ) )
23 13 16 22 3anbi123d 
 |-  ( g = h -> ( ( 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 ) ) <-> ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. w e. Fin A. y e. ( A \ w ) ( h ` y ) = U. ( F ` y ) ) ) )
24 14 ixpeq2dv 
 |-  ( g = h -> X_ y e. A ( g ` y ) = X_ y e. A ( h ` y ) )
25 24 eqeq2d 
 |-  ( g = h -> ( S = X_ y e. A ( g ` y ) <-> S = X_ y e. A ( h ` y ) ) )
26 23 25 anbi12d 
 |-  ( g = h -> ( ( ( 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 ) ) /\ S = X_ y e. A ( g ` y ) ) <-> ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. w e. Fin A. y e. ( A \ w ) ( h ` y ) = U. ( F ` y ) ) /\ S = X_ y e. A ( h ` y ) ) ) )
27 26 cbvexvw 
 |-  ( 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 ) ) /\ S = X_ y e. A ( g ` y ) ) <-> E. h ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. w e. Fin A. y e. ( A \ w ) ( h ` y ) = U. ( F ` y ) ) /\ S = X_ y e. A ( h ` y ) ) )
28 2 12 27 3bitri 
 |-  ( S e. B <-> E. h ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. w e. Fin A. y e. ( A \ w ) ( h ` y ) = U. ( F ` y ) ) /\ S = X_ y e. A ( h ` y ) ) )