Metamath Proof Explorer


Theorem lmmbr2

Description: Express the binary relation "sequence F converges to point P " in a metric space. Definition 1.4-1 of Kreyszig p. 25. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmmbr.2 J = MetOpen D
lmmbr.3 φ D ∞Met X
Assertion lmmbr2 φ F t J P F X 𝑝𝑚 P X x + j k j k dom F F k X F k D P < x

Proof

Step Hyp Ref Expression
1 lmmbr.2 J = MetOpen D
2 lmmbr.3 φ D ∞Met X
3 1 2 lmmbr φ F t J P F X 𝑝𝑚 P X x + y ran F y : y P ball D x
4 df-3an F X 𝑝𝑚 P X x + y ran F y : y P ball D x F X 𝑝𝑚 P X x + y ran F y : y P ball D x
5 uzf : 𝒫
6 ffn : 𝒫 Fn
7 reseq2 y = j F y = F j
8 id y = j y = j
9 7 8 feq12d y = j F y : y P ball D x F j : j P ball D x
10 9 rexrn Fn y ran F y : y P ball D x j F j : j P ball D x
11 5 6 10 mp2b y ran F y : y P ball D x j F j : j P ball D x
12 simp2l D ∞Met X F X 𝑝𝑚 P X x + F X 𝑝𝑚
13 elfvdm D ∞Met X X dom ∞Met
14 13 3ad2ant1 D ∞Met X F X 𝑝𝑚 P X x + X dom ∞Met
15 cnex V
16 elpmg X dom ∞Met V F X 𝑝𝑚 Fun F F × X
17 14 15 16 sylancl D ∞Met X F X 𝑝𝑚 P X x + F X 𝑝𝑚 Fun F F × X
18 12 17 mpbid D ∞Met X F X 𝑝𝑚 P X x + Fun F F × X
19 18 simpld D ∞Met X F X 𝑝𝑚 P X x + Fun F
20 ffvresb Fun F F j : j P ball D x k j k dom F F k P ball D x
21 19 20 syl D ∞Met X F X 𝑝𝑚 P X x + F j : j P ball D x k j k dom F F k P ball D x
22 rpxr x + x *
23 elbl D ∞Met X P X x * F k P ball D x F k X P D F k < x
24 22 23 syl3an3 D ∞Met X P X x + F k P ball D x F k X P D F k < x
25 xmetsym D ∞Met X P X F k X P D F k = F k D P
26 25 breq1d D ∞Met X P X F k X P D F k < x F k D P < x
27 26 3expa D ∞Met X P X F k X P D F k < x F k D P < x
28 27 pm5.32da D ∞Met X P X F k X P D F k < x F k X F k D P < x
29 28 3adant3 D ∞Met X P X x + F k X P D F k < x F k X F k D P < x
30 24 29 bitrd D ∞Met X P X x + F k P ball D x F k X F k D P < x
31 30 3adant2l D ∞Met X F X 𝑝𝑚 P X x + F k P ball D x F k X F k D P < x
32 31 anbi2d D ∞Met X F X 𝑝𝑚 P X x + k dom F F k P ball D x k dom F F k X F k D P < x
33 3anass k dom F F k X F k D P < x k dom F F k X F k D P < x
34 32 33 bitr4di D ∞Met X F X 𝑝𝑚 P X x + k dom F F k P ball D x k dom F F k X F k D P < x
35 34 ralbidv D ∞Met X F X 𝑝𝑚 P X x + k j k dom F F k P ball D x k j k dom F F k X F k D P < x
36 21 35 bitrd D ∞Met X F X 𝑝𝑚 P X x + F j : j P ball D x k j k dom F F k X F k D P < x
37 36 rexbidv D ∞Met X F X 𝑝𝑚 P X x + j F j : j P ball D x j k j k dom F F k X F k D P < x
38 11 37 syl5bb D ∞Met X F X 𝑝𝑚 P X x + y ran F y : y P ball D x j k j k dom F F k X F k D P < x
39 38 3expa D ∞Met X F X 𝑝𝑚 P X x + y ran F y : y P ball D x j k j k dom F F k X F k D P < x
40 39 ralbidva D ∞Met X F X 𝑝𝑚 P X x + y ran F y : y P ball D x x + j k j k dom F F k X F k D P < x
41 40 pm5.32da D ∞Met X F X 𝑝𝑚 P X x + y ran F y : y P ball D x F X 𝑝𝑚 P X x + j k j k dom F F k X F k D P < x
42 2 41 syl φ F X 𝑝𝑚 P X x + y ran F y : y P ball D x F X 𝑝𝑚 P X x + j k j k dom F F k X F k D P < x
43 4 42 syl5bb φ F X 𝑝𝑚 P X x + y ran F y : y P ball D x F X 𝑝𝑚 P X x + j k j k dom F F k X F k D P < x
44 df-3an F X 𝑝𝑚 P X x + j k j k dom F F k X F k D P < x F X 𝑝𝑚 P X x + j k j k dom F F k X F k D P < x
45 43 44 bitr4di φ F X 𝑝𝑚 P X x + y ran F y : y P ball D x F X 𝑝𝑚 P X x + j k j k dom F F k X F k D P < x
46 3 45 bitrd φ F t J P F X 𝑝𝑚 P X x + j k j k dom F F k X F k D P < x