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|ggFnAyAgyFyzFinyAzgy=Fyx=yAgy
Assertion elptr AVGFnAyAGyFyWFinyAWGy=FyyAGyB

Proof

Step Hyp Ref Expression
1 ptbas.1 B=x|ggFnAyAgyFyzFinyAzgy=Fyx=yAgy
2 simp2l AVGFnAyAGyFyWFinyAWGy=FyGFnA
3 simp1 AVGFnAyAGyFyWFinyAWGy=FyAV
4 2 3 fnexd AVGFnAyAGyFyWFinyAWGy=FyGV
5 simp2r AVGFnAyAGyFyWFinyAWGy=FyyAGyFy
6 difeq2 w=WAw=AW
7 6 raleqdv w=WyAwGy=FyyAWGy=Fy
8 7 rspcev WFinyAWGy=FywFinyAwGy=Fy
9 8 3ad2ant3 AVGFnAyAGyFyWFinyAWGy=FywFinyAwGy=Fy
10 2 5 9 3jca AVGFnAyAGyFyWFinyAWGy=FyGFnAyAGyFywFinyAwGy=Fy
11 fveq1 h=Ghy=Gy
12 11 eqcomd h=GGy=hy
13 12 ixpeq2dv h=GyAGy=yAhy
14 13 biantrud h=GhFnAyAhyFywFinyAwhy=FyhFnAyAhyFywFinyAwhy=FyyAGy=yAhy
15 fneq1 h=GhFnAGFnA
16 11 eleq1d h=GhyFyGyFy
17 16 ralbidv h=GyAhyFyyAGyFy
18 11 eqeq1d h=Ghy=FyGy=Fy
19 18 rexralbidv h=GwFinyAwhy=FywFinyAwGy=Fy
20 15 17 19 3anbi123d h=GhFnAyAhyFywFinyAwhy=FyGFnAyAGyFywFinyAwGy=Fy
21 14 20 bitr3d h=GhFnAyAhyFywFinyAwhy=FyyAGy=yAhyGFnAyAGyFywFinyAwGy=Fy
22 4 10 21 spcedv AVGFnAyAGyFyWFinyAWGy=FyhhFnAyAhyFywFinyAwhy=FyyAGy=yAhy
23 1 elpt yAGyBhhFnAyAhyFywFinyAwhy=FyyAGy=yAhy
24 22 23 sylibr AVGFnAyAGyFyWFinyAWGy=FyyAGyB