Theorem climfveqf

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	climfveqf.p	⊢ Ⅎ 𝑘 𝜑
	climfveqf.n	⊢ Ⅎ 𝑘 𝐹
	climfveqf.o	⊢ Ⅎ 𝑘 𝐺
	climfveqf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climfveqf.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	climfveqf.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	climfveqf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climfveqf.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
Assertion	climfveqf	⊢ ( 𝜑 → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		climfveqf.p	⊢ Ⅎ 𝑘 𝜑
2		climfveqf.n	⊢ Ⅎ 𝑘 𝐹
3		climfveqf.o	⊢ Ⅎ 𝑘 𝐺
4		climfveqf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		climfveqf.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
6		climfveqf.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
7		climfveqf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8		climfveqf.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
9		climdm	⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
10	9	biimpi	⊢ ( 𝐹 ∈ dom ⇝ → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
12	11 9	sylibr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
13		nfcv	⊢ Ⅎ 𝑘 𝑗
14	13	nfel1	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
15	1 14	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
16	2 13	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
17	3 13	nffv	⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 )
18	16 17	nfeq	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 )
19	15 18	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
20		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
21	20	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
22		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
23		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑗 ) )
24	22 23	eqeq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) ) )
25	21 24	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) ) ) )
26	19 25 8	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
27	4 5 6 7 26	climeldmeq	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
29	12 28	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ dom ⇝ )
30		climdm	⊢ ( 𝐺 ∈ dom ⇝ ↔ 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
31	29 30	sylib	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) )
32	6	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐺 ∈ 𝑊 )
33	5	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ 𝑉 )
34	7	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝑀 ∈ ℤ )
35	26	eqcomd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
36	35	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
37	4 32 33 34 36	climeq	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐺 ⇝ ( ⇝ ‘ 𝐺 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) )
38	31 37	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) )
39		climuni	⊢ ( ( 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ∧ 𝐹 ⇝ ( ⇝ ‘ 𝐺 ) ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
40	11 38 39	syl2anc	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
41		ndmfv	⊢ ( ¬ 𝐹 ∈ dom ⇝ → ( ⇝ ‘ 𝐹 ) = ∅ )
42	41	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ∅ )
43		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ¬ 𝐹 ∈ dom ⇝ )
44	27	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ) )
45	43 44	mtbid	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ¬ 𝐺 ∈ dom ⇝ )
46		ndmfv	⊢ ( ¬ 𝐺 ∈ dom ⇝ → ( ⇝ ‘ 𝐺 ) = ∅ )
47	45 46	syl	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐺 ) = ∅ )
48	42 47	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )
49	40 48	pm2.61dan	⊢ ( 𝜑 → ( ⇝ ‘ 𝐹 ) = ( ⇝ ‘ 𝐺 ) )