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 φ$
	allbutfifvre.2	$⊢ Z = ℤ_{\geq M}$
	allbutfifvre.3	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
	allbutfifvre.4	$⊢ D = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
	allbutfifvre.5	$⊢ φ \to X \in D$
Assertion	allbutfifvre	$⊢ φ \to \exists n \in Z \forall m \in ℤ_{\geq n} F (m) (X) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		allbutfifvre.1	$⊢ Ⅎ m φ$
2		allbutfifvre.2	$⊢ Z = ℤ_{\geq M}$
3		allbutfifvre.3	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
4		allbutfifvre.4	$⊢ D = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
5		allbutfifvre.5	$⊢ φ \to X \in D$
6	5 4	eleqtrdi	$⊢ φ \to X \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
7		eqid	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
8	2 7	allbutfi	$⊢ X \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow \exists n \in Z \forall m \in ℤ_{\geq n} X \in dom F (m)$
9	6 8	sylib	$⊢ φ \to \exists n \in Z \forall m \in ℤ_{\geq n} X \in dom F (m)$
10		nfv	$⊢ Ⅎ m n \in Z$
11	1 10	nfan	$⊢ Ⅎ m (φ \land n \in Z)$
12		simpll	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to φ$
13	2	uztrn2	$⊢ (n \in Z \land j \in ℤ_{\geq n}) \to j \in Z$
14	13	ssd	$⊢ n \in Z \to ℤ_{\geq n} \subseteq Z$
15	14	sselda	$⊢ (n \in Z \land m \in ℤ_{\geq n}) \to m \in Z$
16	15	adantll	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to m \in Z$
17	3	ffvelrnda	$⊢ ((φ \land m \in Z) \land X \in dom F (m)) \to F (m) (X) \in ℝ$
18	17	ex	$⊢ (φ \land m \in Z) \to (X \in dom F (m) \to F (m) (X) \in ℝ)$
19	12 16 18	syl2anc	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to (X \in dom F (m) \to F (m) (X) \in ℝ)$
20	11 19	ralimdaa	$⊢ (φ \land n \in Z) \to (\forall m \in ℤ_{\geq n} X \in dom F (m) \to \forall m \in ℤ_{\geq n} F (m) (X) \in ℝ)$
21	20	reximdva	$⊢ φ \to (\exists n \in Z \forall m \in ℤ_{\geq n} X \in dom F (m) \to \exists n \in Z \forall m \in ℤ_{\geq n} F (m) (X) \in ℝ)$
22	9 21	mpd	$⊢ φ \to \exists n \in Z \forall m \in ℤ_{\geq n} F (m) (X) \in ℝ$

Metamath Proof Explorer

Theorem allbutfifvre

Proof