# Metamath Proof Explorer

## Theorem allbutfifvre

Description: Given a sequence of real-valued functions, and X that belongs to all but finitely many domains, then its function value is ultimately a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses allbutfifvre.1 ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{\phi }$
allbutfifvre.2 ${⊢}{Z}={ℤ}_{\ge {M}}$
allbutfifvre.3 ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {F}\left({m}\right):\mathrm{dom}{F}\left({m}\right)⟶ℝ$
allbutfifvre.4 ${⊢}{D}=\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
allbutfifvre.5 ${⊢}{\phi }\to {X}\in {D}$
Assertion allbutfifvre ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({X}\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 allbutfifvre.1 ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{\phi }$
2 allbutfifvre.2 ${⊢}{Z}={ℤ}_{\ge {M}}$
3 allbutfifvre.3 ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {F}\left({m}\right):\mathrm{dom}{F}\left({m}\right)⟶ℝ$
4 allbutfifvre.4 ${⊢}{D}=\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
5 allbutfifvre.5 ${⊢}{\phi }\to {X}\in {D}$
6 5 4 eleqtrdi ${⊢}{\phi }\to {X}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
7 eqid ${⊢}\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)=\bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)$
8 2 7 allbutfi ${⊢}{X}\in \bigcup _{{n}\in {Z}}\bigcap _{{m}\in {ℤ}_{\ge {n}}}\mathrm{dom}{F}\left({m}\right)↔\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{X}\in \mathrm{dom}{F}\left({m}\right)$
9 6 8 sylib ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{X}\in \mathrm{dom}{F}\left({m}\right)$
10 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{n}\in {Z}$
11 1 10 nfan ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {n}\in {Z}\right)$
12 simpll ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {\phi }$
13 2 uztrn2 ${⊢}\left({n}\in {Z}\wedge {j}\in {ℤ}_{\ge {n}}\right)\to {j}\in {Z}$
14 13 ssd ${⊢}{n}\in {Z}\to {ℤ}_{\ge {n}}\subseteq {Z}$
15 14 sselda ${⊢}\left({n}\in {Z}\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
16 15 adantll ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to {m}\in {Z}$
17 3 ffvelrnda ${⊢}\left(\left({\phi }\wedge {m}\in {Z}\right)\wedge {X}\in \mathrm{dom}{F}\left({m}\right)\right)\to {F}\left({m}\right)\left({X}\right)\in ℝ$
18 17 ex ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to \left({X}\in \mathrm{dom}{F}\left({m}\right)\to {F}\left({m}\right)\left({X}\right)\in ℝ\right)$
19 12 16 18 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {m}\in {ℤ}_{\ge {n}}\right)\to \left({X}\in \mathrm{dom}{F}\left({m}\right)\to {F}\left({m}\right)\left({X}\right)\in ℝ\right)$
20 11 19 ralimdaa ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left(\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{X}\in \mathrm{dom}{F}\left({m}\right)\to \forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({X}\right)\in ℝ\right)$
21 20 reximdva ${⊢}{\phi }\to \left(\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{X}\in \mathrm{dom}{F}\left({m}\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({X}\right)\in ℝ\right)$
22 9 21 mpd ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {n}}\phantom{\rule{.4em}{0ex}}{F}\left({m}\right)\left({X}\right)\in ℝ$