Theorem climeqf

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

	Ref	Expression
Hypotheses	climeqf.p	$$⊢Ⅎk\phi$$
	climeqf.k	$$⊢\underset{\_}{Ⅎ}kF$$
	climeqf.n	$$⊢\underset{\_}{Ⅎ}kG$$
	climeqf.m	$$⊢\phi \to M\in \mathbb{Z}$$
	climeqf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climeqf.f	$$⊢\phi \to F\in V$$
	climeqf.g	$$⊢\phi \to G\in W$$
	climeqf.e	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=G\left(k\right)$$
Assertion	climeqf	$$⊢\phi \to \left(F⇝A\leftrightarrow G⇝A\right)$$

Proof

Step	Hyp	Ref	Expression
1		climeqf.p	$$⊢Ⅎk\phi$$
2		climeqf.k	$$⊢\underset{\_}{Ⅎ}kF$$
3		climeqf.n	$$⊢\underset{\_}{Ⅎ}kG$$
4		climeqf.m	$$⊢\phi \to M\in \mathbb{Z}$$
5		climeqf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
6		climeqf.f	$$⊢\phi \to F\in V$$
7		climeqf.g	$$⊢\phi \to G\in W$$
8		climeqf.e	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=G\left(k\right)$$
9		nfv	$$⊢Ⅎkj\in Z$$
10	1 9	nfan	$$⊢Ⅎk\left(\phi \wedge j\in Z\right)$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
12	2 11	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)$$
13	3 11	nffv	$$⊢\underset{\_}{Ⅎ}kG\left(j\right)$$
14	12 13	nfeq	$$⊢ℲkF\left(j\right)=G\left(j\right)$$
15	10 14	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in Z\right)\to F\left(j\right)=G\left(j\right)\right)$$
16		eleq1w	$$⊢k=j\to \left(k\in Z\leftrightarrow j\in Z\right)$$
17	16	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in Z\right)\leftrightarrow \left(\phi \wedge j\in Z\right)\right)$$
18		fveq2	$$⊢k=j\to F\left(k\right)=F\left(j\right)$$
19		fveq2	$$⊢k=j\to G\left(k\right)=G\left(j\right)$$
20	18 19	eqeq12d	$$⊢k=j\to \left(F\left(k\right)=G\left(k\right)\leftrightarrow F\left(j\right)=G\left(j\right)\right)$$
21	17 20	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in Z\right)\to F\left(k\right)=G\left(k\right)\right)\leftrightarrow \left(\left(\phi \wedge j\in Z\right)\to F\left(j\right)=G\left(j\right)\right)\right)$$
22	15 21 8	chvarfv	$$⊢\left(\phi \wedge j\in Z\right)\to F\left(j\right)=G\left(j\right)$$
23	5 6 7 4 22	climeq	$$⊢\phi \to \left(F⇝A\leftrightarrow G⇝A\right)$$