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 | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
Assertion elpt S B h h Fn A y A h y F y w Fin y A w h y = F y S = y A h y

Proof

Step Hyp Ref Expression
1 ptbas.1 B = x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
2 1 eleq2i S B S x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
3 simpr g Fn A y A g y F y z Fin y A z g y = F y S = y A g y S = y A g y
4 ixpexg y A g y V y A g y V
5 fvexd y A g y V
6 4 5 mprg y A g y V
7 3 6 eqeltrdi g Fn A y A g y F y z Fin y A z g y = F y S = y A g y S V
8 7 exlimiv g g Fn A y A g y F y z Fin y A z g y = F y S = y A g y S V
9 eqeq1 x = S x = y A g y S = y A g y
10 9 anbi2d x = S g Fn A y A g y F y z Fin y A z g y = F y x = y A g y g Fn A y A g y F y z Fin y A z g y = F y S = y A g y
11 10 exbidv x = S g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y g g Fn A y A g y F y z Fin y A z g y = F y S = y A g y
12 8 11 elab3 S x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y g g Fn A y A g y F y z Fin y A z g y = F y S = y 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 F y h y F y
16 15 ralbidv g = h y A g y F y y A h y F y
17 14 eqeq1d g = h g y = F y h y = F y
18 17 rexralbidv g = h z Fin y A z g y = F y z Fin y A z h y = F y
19 difeq2 z = w A z = A w
20 19 raleqdv z = w y A z h y = F y y A w h y = F y
21 20 cbvrexvw z Fin y A z h y = F y w Fin y A w h y = F y
22 18 21 bitrdi g = h z Fin y A z g y = F y w Fin y A w h y = F y
23 13 16 22 3anbi123d g = h g Fn A y A g y F y z Fin y A z g y = F y h Fn A y A h y F y w Fin y A w h y = F y
24 14 ixpeq2dv g = h y A g y = y A h y
25 24 eqeq2d g = h S = y A g y S = y A h y
26 23 25 anbi12d g = h g Fn A y A g y F y z Fin y A z g y = F y S = y A g y h Fn A y A h y F y w Fin y A w h y = F y S = y A h y
27 26 cbvexvw g g Fn A y A g y F y z Fin y A z g y = F y S = y A g y h h Fn A y A h y F y w Fin y A w h y = F y S = y A h y
28 2 12 27 3bitri S B h h Fn A y A h y F y w Fin y A w h y = F y S = y A h y