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 fnex 
 |-  ( ( G Fn A /\ A e. V ) -> G e. _V )
5 2 3 4 syl2anc 
 |-  ( ( 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 )
6 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 ) )
7 difeq2 
 |-  ( w = W -> ( A \ w ) = ( A \ W ) )
8 7 raleqdv 
 |-  ( w = W -> ( A. y e. ( A \ w ) ( G ` y ) = U. ( F ` y ) <-> A. y e. ( A \ W ) ( G ` y ) = U. ( F ` y ) ) )
9 8 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 ) )
10 9 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 ) )
11 2 6 10 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 ) ) )
12 fveq1 
 |-  ( h = G -> ( h ` y ) = ( G ` y ) )
13 12 eqcomd 
 |-  ( h = G -> ( G ` y ) = ( h ` y ) )
14 13 ixpeq2dv 
 |-  ( h = G -> X_ y e. A ( G ` y ) = X_ y e. A ( h ` y ) )
15 14 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 ) ) ) )
16 fneq1 
 |-  ( h = G -> ( h Fn A <-> G Fn A ) )
17 12 eleq1d 
 |-  ( h = G -> ( ( h ` y ) e. ( F ` y ) <-> ( G ` y ) e. ( F ` y ) ) )
18 17 ralbidv 
 |-  ( h = G -> ( A. y e. A ( h ` y ) e. ( F ` y ) <-> A. y e. A ( G ` y ) e. ( F ` y ) ) )
19 12 eqeq1d 
 |-  ( h = G -> ( ( h ` y ) = U. ( F ` y ) <-> ( G ` y ) = U. ( F ` y ) ) )
20 19 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 ) ) )
21 16 18 20 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 ) ) ) )
22 15 21 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 ) ) ) )
23 5 11 22 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 ) ) )
24 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 ) ) )
25 23 24 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 )