Metamath Proof Explorer

Theorem elptr

Description: A basic open set in 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 elptr 
|- ( ( A e. V /\ ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) ) -> X_ y e. A ( G ` y ) 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 simp2l 
 |-  ( ( A e. V /\ ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) ) -> G Fn A )
3 simp1 
 |-  ( ( A e. V /\ ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) ) -> A e. V )
4 2 3 fnexd 
 |-  ( ( A e. V /\ ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) ) -> G e. _V )
5 simp2r 
 |-  ( ( A e. V /\ ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) ) -> A. y e. A ( G ` y ) e. ( F ` y ) )
6 difeq2 
 |-  ( w = W -> ( A \ w ) = ( A \ W ) )
7 6 raleqdv 
 |-  ( w = W -> ( A. y e. ( A \ w ) ( G ` y ) = U. ( F ` y ) <-> A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) )
8 7 rspcev 
 |-  ( ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) -> E. w e. Fin A. y e. ( A \ w ) ( G ` y ) = U. ( F ` y ) )
9 8 3ad2ant3 
 |-  ( ( A e. V /\ ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) ) -> E. w e. Fin A. y e. ( A \ w ) ( G ` y ) = U. ( F ` y ) )
10 2 5 9 3jca 
 |-  ( ( A e. V /\ ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) ) -> ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) /\ E. w e. Fin A. y e. ( A \ w ) ( G ` y ) = U. ( F ` y ) ) )
11 fveq1 
 |-  ( h = G -> ( h ` y ) = ( G ` y ) )
12 11 eqcomd 
 |-  ( h = G -> ( G ` y ) = ( h ` y ) )
13 12 ixpeq2dv 
 |-  ( h = G -> X_ y e. A ( G ` y ) = X_ y e. A ( h ` y ) )
14 13 biantrud 
 |-  ( h = G -> ( ( 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 ) ) <-> ( ( 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 ) ) /\ X_ y e. A ( G ` y ) = X_ y e. A ( h ` y ) ) ) )
15 fneq1 
 |-  ( h = G -> ( h Fn A <-> G Fn A ) )
16 11 eleq1d 
 |-  ( h = G -> ( ( h ` y ) e. ( F ` y ) <-> ( G ` y ) e. ( F ` y ) ) )
17 16 ralbidv 
 |-  ( h = G -> ( A. y e. A ( h ` y ) e. ( F ` y ) <-> A. y e. A ( G ` y ) e. ( F ` y ) ) )
18 11 eqeq1d 
 |-  ( h = G -> ( ( h ` y ) = U. ( F ` y ) <-> ( G ` y ) = U. ( F ` y ) ) )
19 18 rexralbidv 
 |-  ( h = G -> ( E. w e. Fin A. y e. ( A \ w ) ( h ` y ) = U. ( F ` y ) <-> E. w e. Fin A. y e. ( A \ w ) ( G ` y ) = U. ( F ` y ) ) )
20 15 17 19 3anbi123d 
 |-  ( h = G -> ( ( 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 ) ) <-> ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) /\ E. w e. Fin A. y e. ( A \ w ) ( G ` y ) = U. ( F ` y ) ) ) )
21 14 20 bitr3d 
 |-  ( h = G -> ( ( ( 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 ) ) /\ X_ y e. A ( G ` y ) = X_ y e. A ( h ` y ) ) <-> ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) /\ E. w e. Fin A. y e. ( A \ w ) ( G ` y ) = U. ( F ` y ) ) ) )
22 4 10 21 spcedv 
 |-  ( ( A e. V /\ ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` 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 ) ) /\ X_ y e. A ( G ` y ) = X_ y e. A ( h ` y ) ) )
23 1 elpt 
 |-  ( X_ y e. A ( G ` y ) 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 ) ) /\ X_ y e. A ( G ` y ) = X_ y e. A ( h ` y ) ) )
24 22 23 sylibr 
 |-  ( ( A e. V /\ ( G Fn A /\ A. y e. A ( G ` y ) e. ( F ` y ) ) /\ ( W e. Fin /\ A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) ) -> X_ y e. A ( G ` y ) e. B )