# Metamath Proof Explorer

## Theorem lmmbrf

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 presupposes that F is a function. (Contributed by NM, 20-Jul-2007) (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)$
lmmbr3.5 ${⊢}{Z}={ℤ}_{\ge {M}}$
lmmbr3.6 ${⊢}{\phi }\to {M}\in ℤ$
lmmbrf.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={A}$
lmmbrf.8 ${⊢}{\phi }\to {F}:{Z}⟶{X}$
Assertion lmmbrf

### 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 lmmbr3.5 ${⊢}{Z}={ℤ}_{\ge {M}}$
4 lmmbr3.6 ${⊢}{\phi }\to {M}\in ℤ$
5 lmmbrf.7 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={A}$
6 lmmbrf.8 ${⊢}{\phi }\to {F}:{Z}⟶{X}$
7 elfvdm ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {X}\in \mathrm{dom}\mathrm{\infty Met}$
8 cnex ${⊢}ℂ\in \mathrm{V}$
9 7 8 jctir ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({X}\in \mathrm{dom}\mathrm{\infty Met}\wedge ℂ\in \mathrm{V}\right)$
10 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
11 zsscn ${⊢}ℤ\subseteq ℂ$
12 10 11 sstri ${⊢}{ℤ}_{\ge {M}}\subseteq ℂ$
13 3 12 eqsstri ${⊢}{Z}\subseteq ℂ$
14 13 jctr ${⊢}{F}:{Z}⟶{X}\to \left({F}:{Z}⟶{X}\wedge {Z}\subseteq ℂ\right)$
15 elpm2r ${⊢}\left(\left({X}\in \mathrm{dom}\mathrm{\infty Met}\wedge ℂ\in \mathrm{V}\right)\wedge \left({F}:{Z}⟶{X}\wedge {Z}\subseteq ℂ\right)\right)\to {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)$
16 9 14 15 syl2an ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}:{Z}⟶{X}\right)\to {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)$
17 2 6 16 syl2anc ${⊢}{\phi }\to {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)$
18 17 biantrurd ${⊢}{\phi }\to \left(\left({P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\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({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \left({P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\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)\right)$
19 3 uztrn2 ${⊢}\left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {Z}$
20 19 adantll ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {Z}$
21 5 oveq1d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right){D}{P}={A}{D}{P}$
22 21 breq1d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({F}\left({k}\right){D}{P}<{x}↔{A}{D}{P}<{x}\right)$
23 22 adantrl ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge {k}\in {Z}\right)\right)\to \left({F}\left({k}\right){D}{P}<{x}↔{A}{D}{P}<{x}\right)$
24 6 fdmd ${⊢}{\phi }\to \mathrm{dom}{F}={Z}$
25 24 eleq2d ${⊢}{\phi }\to \left({k}\in \mathrm{dom}{F}↔{k}\in {Z}\right)$
26 25 biimpar ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {k}\in \mathrm{dom}{F}$
27 6 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in {X}$
28 26 27 jca ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\right)$
29 28 biantrurd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({F}\left({k}\right){D}{P}<{x}↔\left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\right)\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
30 df-3an ${⊢}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)↔\left(\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\right)\wedge {F}\left({k}\right){D}{P}<{x}\right)$
31 29 30 syl6bbr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({F}\left({k}\right){D}{P}<{x}↔\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
32 31 adantrl ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge {k}\in {Z}\right)\right)\to \left({F}\left({k}\right){D}{P}<{x}↔\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
33 23 32 bitr3d ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge {k}\in {Z}\right)\right)\to \left({A}{D}{P}<{x}↔\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
34 33 anassrs ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {Z}\right)\to \left({A}{D}{P}<{x}↔\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
35 20 34 syldan ${⊢}\left(\left({\phi }\wedge {j}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left({A}{D}{P}<{x}↔\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{P}<{x}\right)\right)$
36 35 ralbidva ${⊢}\left({\phi }\wedge {j}\in {Z}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{A}{D}{P}<{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 rexbidva ${⊢}{\phi }\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{A}{D}{P}<{x}↔\exists {j}\in {Z}\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 37 ralbidv ${⊢}{\phi }\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{A}{D}{P}<{x}↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\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 anbi2d ${⊢}{\phi }\to \left(\left({P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{A}{D}{P}<{x}\right)↔\left({P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\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)$
40 1 2 3 4 lmmbr3
41 3anass ${⊢}\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\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({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \left({P}\in {X}\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\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 40 41 syl6bb
43 18 39 42 3bitr4rd