# Metamath Proof Explorer

## Theorem lmff

Description: If F converges, there is some upper integer set on which F is a total function. (Contributed by Mario Carneiro, 31-Dec-2013)

Ref Expression
Hypotheses lmff.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
lmff.3 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
lmff.4 ${⊢}{\phi }\to {M}\in ℤ$
lmff.5
Assertion lmff ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}$

### Proof

Step Hyp Ref Expression
1 lmff.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 lmff.3 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
3 lmff.4 ${⊢}{\phi }\to {M}\in ℤ$
4 lmff.5
5 eldm2g
6 5 ibi
7 4 6 syl
8 df-br
9 8 exbii
10 7 9 sylibr
11 lmcl
12 2 11 sylan
13 eleq2 ${⊢}{j}={X}\to \left({y}\in {j}↔{y}\in {X}\right)$
14 feq3 ${⊢}{j}={X}\to \left(\left({{F}↾}_{{x}}\right):{x}⟶{j}↔\left({{F}↾}_{{x}}\right):{x}⟶{X}\right)$
15 14 rexbidv ${⊢}{j}={X}\to \left(\exists {x}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{x}}\right):{x}⟶{j}↔\exists {x}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{x}}\right):{x}⟶{X}\right)$
16 13 15 imbi12d ${⊢}{j}={X}\to \left(\left({y}\in {j}\to \exists {x}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{x}}\right):{x}⟶{j}\right)↔\left({y}\in {X}\to \exists {x}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{x}}\right):{x}⟶{X}\right)\right)$
17 2 lmbr
18 17 biimpa
19 18 simp3d
20 toponmax ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}\in {J}$
21 2 20 syl ${⊢}{\phi }\to {X}\in {J}$
23 16 19 22 rspcdva
24 12 23 mpd
25 10 24 exlimddv ${⊢}{\phi }\to \exists {x}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{x}}\right):{x}⟶{X}$
26 uzf ${⊢}{ℤ}_{\ge }:ℤ⟶𝒫ℤ$
27 ffn ${⊢}{ℤ}_{\ge }:ℤ⟶𝒫ℤ\to {ℤ}_{\ge }Fnℤ$
28 reseq2 ${⊢}{x}={ℤ}_{\ge {j}}\to {{F}↾}_{{x}}={{F}↾}_{{ℤ}_{\ge {j}}}$
29 id ${⊢}{x}={ℤ}_{\ge {j}}\to {x}={ℤ}_{\ge {j}}$
30 28 29 feq12d ${⊢}{x}={ℤ}_{\ge {j}}\to \left(\left({{F}↾}_{{x}}\right):{x}⟶{X}↔\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)$
31 30 rexrn ${⊢}{ℤ}_{\ge }Fnℤ\to \left(\exists {x}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{x}}\right):{x}⟶{X}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)$
32 26 27 31 mp2b ${⊢}\exists {x}\in \mathrm{ran}{ℤ}_{\ge }\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{x}}\right):{x}⟶{X}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}$
33 25 32 sylib ${⊢}{\phi }\to \exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}$
34 1 rexuz3 ${⊢}{M}\in ℤ\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{dom}{F}\wedge {F}\left({x}\right)\in {X}\right)↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{dom}{F}\wedge {F}\left({x}\right)\in {X}\right)\right)$
35 3 34 syl ${⊢}{\phi }\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{dom}{F}\wedge {F}\left({x}\right)\in {X}\right)↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{dom}{F}\wedge {F}\left({x}\right)\in {X}\right)\right)$
36 18 simp1d
37 10 36 exlimddv ${⊢}{\phi }\to {F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)$
38 pmfun ${⊢}{F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\to \mathrm{Fun}{F}$
39 37 38 syl ${⊢}{\phi }\to \mathrm{Fun}{F}$
40 ffvresb ${⊢}\mathrm{Fun}{F}\to \left(\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}↔\forall {x}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{dom}{F}\wedge {F}\left({x}\right)\in {X}\right)\right)$
41 39 40 syl ${⊢}{\phi }\to \left(\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}↔\forall {x}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{dom}{F}\wedge {F}\left({x}\right)\in {X}\right)\right)$
42 41 rexbidv ${⊢}{\phi }\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}↔\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{dom}{F}\wedge {F}\left({x}\right)\in {X}\right)\right)$
43 41 rexbidv ${⊢}{\phi }\to \left(\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({x}\in \mathrm{dom}{F}\wedge {F}\left({x}\right)\in {X}\right)\right)$
44 35 42 43 3bitr4d ${⊢}{\phi }\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}↔\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)$
45 33 44 mpbird ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}$