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	⊢ Ⅎ 𝑚 𝜑
	allbutfifvre.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	allbutfifvre.3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
	allbutfifvre.4	⊢ 𝐷 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
	allbutfifvre.5	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion	allbutfifvre	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		allbutfifvre.1	⊢ Ⅎ 𝑚 𝜑
2		allbutfifvre.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		allbutfifvre.3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
4		allbutfifvre.4	⊢ 𝐷 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
5		allbutfifvre.5	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
6	5 4	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) )
7		eqid	⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
8	2 7	allbutfi	⊢ ( 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) )
9	6 8	sylib	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) )
10		nfv	⊢ Ⅎ 𝑚 𝑛 ∈ 𝑍
11	1 10	nfan	⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
12		simpll	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
13	2	uztrn2	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑗 ∈ 𝑍 )
14	13	ssd	⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
15	14	sselda	⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
16	15	adantll	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
17	3	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ )
18	17	ex	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ ) )
19	12 16 18	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ ) )
20	11 19	ralimdaa	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ ) )
21	20	reximdva	⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ dom ( 𝐹 ‘ 𝑚 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ ) )
22	9 21	mpd	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ∈ ℝ )