# Metamath Proof Explorer

## Theorem lmcvg

Description: Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypotheses lmcvg.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
lmcvg.3 ${⊢}{\phi }\to {P}\in {U}$
lmcvg.4 ${⊢}{\phi }\to {M}\in ℤ$
lmcvg.5
lmcvg.6 ${⊢}{\phi }\to {U}\in {J}$
Assertion lmcvg ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {U}$

### Proof

Step Hyp Ref Expression
1 lmcvg.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 lmcvg.3 ${⊢}{\phi }\to {P}\in {U}$
3 lmcvg.4 ${⊢}{\phi }\to {M}\in ℤ$
4 lmcvg.5
5 lmcvg.6 ${⊢}{\phi }\to {U}\in {J}$
6 eleq2 ${⊢}{u}={U}\to \left({P}\in {u}↔{P}\in {U}\right)$
7 eleq2 ${⊢}{u}={U}\to \left({F}\left({k}\right)\in {u}↔{F}\left({k}\right)\in {U}\right)$
8 7 rexralbidv ${⊢}{u}={U}\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}↔\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {U}\right)$
9 6 8 imbi12d ${⊢}{u}={U}\to \left(\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)↔\left({P}\in {U}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {U}\right)\right)$
10 lmrcl
11 4 10 syl ${⊢}{\phi }\to {J}\in \mathrm{Top}$
12 toptopon2 ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
13 11 12 sylib ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
14 13 1 3 lmbr2
15 4 14 mpbid ${⊢}{\phi }\to \left({F}\in \left(\bigcup {J}{↑}_{𝑝𝑚}ℂ\right)\wedge {P}\in \bigcup {J}\wedge \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \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 {u}\right)\right)\right)$
16 15 simp3d ${⊢}{\phi }\to \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \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 {u}\right)\right)$
17 simpr ${⊢}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\to {F}\left({k}\right)\in {u}$
18 17 ralimi ${⊢}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {u}\right)\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}$
19 18 reximi ${⊢}\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 {u}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}$
20 19 imim2i ${⊢}\left({P}\in {u}\to \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 {u}\right)\right)\to \left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)$
21 20 ralimi ${⊢}\forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \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 {u}\right)\right)\to \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)$
22 16 21 syl ${⊢}{\phi }\to \forall {u}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {u}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {u}\right)$
23 9 22 5 rspcdva ${⊢}{\phi }\to \left({P}\in {U}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {U}\right)$
24 2 23 mpd ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in {U}$