Metamath Proof Explorer


Theorem lmbr3

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses lmbr3.1 _ k F
lmbr3.2 φ J TopOn X
Assertion lmbr3 φ F t J P F X 𝑝𝑚 P X u J P u j k j k dom F F k u

Proof

Step Hyp Ref Expression
1 lmbr3.1 _ k F
2 lmbr3.2 φ J TopOn X
3 2 lmbr3v φ F t J P F X 𝑝𝑚 P X v J P v i l i l dom F F l v
4 eleq2w v = u P v P u
5 eleq2w v = u F l v F l u
6 5 anbi2d v = u l dom F F l v l dom F F l u
7 6 rexralbidv v = u i l i l dom F F l v i l i l dom F F l u
8 fveq2 i = j i = j
9 8 raleqdv i = j l i l dom F F l u l j l dom F F l u
10 nfcv _ k l
11 1 nfdm _ k dom F
12 10 11 nfel k l dom F
13 1 10 nffv _ k F l
14 nfcv _ k u
15 13 14 nfel k F l u
16 12 15 nfan k l dom F F l u
17 nfv l k dom F F k u
18 eleq1w l = k l dom F k dom F
19 fveq2 l = k F l = F k
20 19 eleq1d l = k F l u F k u
21 18 20 anbi12d l = k l dom F F l u k dom F F k u
22 16 17 21 cbvralw l j l dom F F l u k j k dom F F k u
23 9 22 bitrdi i = j l i l dom F F l u k j k dom F F k u
24 23 cbvrexvw i l i l dom F F l u j k j k dom F F k u
25 7 24 bitrdi v = u i l i l dom F F l v j k j k dom F F k u
26 4 25 imbi12d v = u P v i l i l dom F F l v P u j k j k dom F F k u
27 26 cbvralvw v J P v i l i l dom F F l v u J P u j k j k dom F F k u
28 27 3anbi3i F X 𝑝𝑚 P X v J P v i l i l dom F F l v F X 𝑝𝑚 P X u J P u j k j k dom F F k u
29 3 28 bitrdi φ F t J P F X 𝑝𝑚 P X u J P u j k j k dom F F k u