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}=\mathrm{MetOpen}\left({D}\right)$
lmmbr.3 ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
Assertion lmmbr2

Proof

Step Hyp Ref Expression
1 lmmbr.2 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
2 lmmbr.3 ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
3 1 2 lmmbr
4 df-3an ${⊢}\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}\right)↔\left(\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}\right)$
5 uzf ${⊢}{ℤ}_{\ge }:ℤ⟶𝒫ℤ$
6 ffn ${⊢}{ℤ}_{\ge }:ℤ⟶𝒫ℤ\to {ℤ}_{\ge }Fnℤ$
7 reseq2 ${⊢}{y}={ℤ}_{\ge {j}}\to {{F}↾}_{{y}}={{F}↾}_{{ℤ}_{\ge {j}}}$
8 id ${⊢}{y}={ℤ}_{\ge {j}}\to {y}={ℤ}_{\ge {j}}$
9 7 8 feq12d ${⊢}{y}={ℤ}_{\ge {j}}\to \left(\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}↔\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{P}\mathrm{ball}\left({D}\right){x}\right)$
10 9 rexrn ${⊢}{ℤ}_{\ge }Fnℤ\to \left(\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{P}\mathrm{ball}\left({D}\right){x}\right)$
11 5 6 10 mp2b ${⊢}\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{P}\mathrm{ball}\left({D}\right){x}$
12 simp2l ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)$
13 elfvdm ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {X}\in \mathrm{dom}\mathrm{\infty Met}$
14 13 3ad2ant1 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to {X}\in \mathrm{dom}\mathrm{\infty Met}$
15 cnex ${⊢}ℂ\in \mathrm{V}$
16 elpmg ${⊢}\left({X}\in \mathrm{dom}\mathrm{\infty Met}\wedge ℂ\in \mathrm{V}\right)\to \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)↔\left(\mathrm{Fun}{F}\wedge {F}\subseteq ℂ×{X}\right)\right)$
17 14 15 16 sylancl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)↔\left(\mathrm{Fun}{F}\wedge {F}\subseteq ℂ×{X}\right)\right)$
18 12 17 mpbid ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\mathrm{Fun}{F}\wedge {F}\subseteq ℂ×{X}\right)$
19 18 simpld ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{Fun}{F}$
20 ffvresb ${⊢}\mathrm{Fun}{F}\to \left(\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{P}\mathrm{ball}\left({D}\right){x}↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({P}\mathrm{ball}\left({D}\right){x}\right)\right)\right)$
21 19 20 syl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{P}\mathrm{ball}\left({D}\right){x}↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({P}\mathrm{ball}\left({D}\right){x}\right)\right)\right)$
22 rpxr ${⊢}{x}\in {ℝ}^{+}\to {x}\in {ℝ}^{*}$
23 elbl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {x}\in {ℝ}^{*}\right)\to \left({F}\left({k}\right)\in \left({P}\mathrm{ball}\left({D}\right){x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {P}{D}{F}\left({k}\right)<{x}\right)\right)$
24 22 23 syl3an3 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {x}\in {ℝ}^{+}\right)\to \left({F}\left({k}\right)\in \left({P}\mathrm{ball}\left({D}\right){x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {P}{D}{F}\left({k}\right)<{x}\right)\right)$
25 xmetsym ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {F}\left({k}\right)\in {X}\right)\to {P}{D}{F}\left({k}\right)={F}\left({k}\right){D}{P}$
26 25 breq1d ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {F}\left({k}\right)\in {X}\right)\to \left({P}{D}{F}\left({k}\right)<{x}↔{F}\left({k}\right){D}{P}<{x}\right)$
27 26 3expa ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\right)\wedge {F}\left({k}\right)\in {X}\right)\to \left({P}{D}{F}\left({k}\right)<{x}↔{F}\left({k}\right){D}{P}<{x}\right)$
28 27 pm5.32da ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\right)\to \left(\left({F}\left({k}\right)\in {X}\wedge {P}{D}{F}\left({k}\right)<{x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
29 28 3adant3 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {x}\in {ℝ}^{+}\right)\to \left(\left({F}\left({k}\right)\in {X}\wedge {P}{D}{F}\left({k}\right)<{x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
30 24 29 bitrd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {x}\in {ℝ}^{+}\right)\to \left({F}\left({k}\right)\in \left({P}\mathrm{ball}\left({D}\right){x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
31 30 3adant2l ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left({F}\left({k}\right)\in \left({P}\mathrm{ball}\left({D}\right){x}\right)↔\left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
32 31 anbi2d ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({P}\mathrm{ball}\left({D}\right){x}\right)\right)↔\left({k}\in \mathrm{dom}{F}\wedge \left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)\right)$
33 3anass ${⊢}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)↔\left({k}\in \mathrm{dom}{F}\wedge \left({F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
34 32 33 syl6bbr ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({P}\mathrm{ball}\left({D}\right){x}\right)\right)↔\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
35 34 ralbidv ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in \left({P}\mathrm{ball}\left({D}\right){x}\right)\right)↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
36 21 35 bitrd ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{P}\mathrm{ball}\left({D}\right){x}↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
37 36 rexbidv ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{P}\mathrm{ball}\left({D}\right){x}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
38 11 37 syl5bb ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
39 38 3expa ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
40 39 ralbidva ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\right)\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
41 40 pm5.32da ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(\left(\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}\right)↔\left(\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)\right)$
42 2 41 syl ${⊢}{\phi }\to \left(\left(\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}\right)↔\left(\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)\right)$
43 4 42 syl5bb ${⊢}{\phi }\to \left(\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}\right)↔\left(\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)\right)$
44 df-3an ${⊢}\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)↔\left(\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
45 43 44 syl6bbr ${⊢}{\phi }\to \left(\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{y}}\right):{y}⟶{P}\mathrm{ball}\left({D}\right){x}\right)↔\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)\right)$
46 3 45 bitrd