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	$⊢ Ⅎ k φ$
	climfveqf.n	$⊢ \underline{Ⅎ} k F$
	climfveqf.o	$⊢ \underline{Ⅎ} k G$
	climfveqf.z	$⊢ Z = ℤ_{\geq M}$
	climfveqf.f	$⊢ φ \to F \in V$
	climfveqf.g	$⊢ φ \to G \in W$
	climfveqf.m	$⊢ φ \to M \in ℤ$
	climfveqf.e	$⊢ (φ \land k \in Z) \to F (k) = G (k)$
Assertion	climfveqf	$⊢ φ \to ⇝ (F) = ⇝ (G)$

Proof

Step	Hyp	Ref	Expression
1		climfveqf.p	$⊢ Ⅎ k φ$
2		climfveqf.n	$⊢ \underline{Ⅎ} k F$
3		climfveqf.o	$⊢ \underline{Ⅎ} k G$
4		climfveqf.z	$⊢ Z = ℤ_{\geq M}$
5		climfveqf.f	$⊢ φ \to F \in V$
6		climfveqf.g	$⊢ φ \to G \in W$
7		climfveqf.m	$⊢ φ \to M \in ℤ$
8		climfveqf.e	$⊢ (φ \land k \in Z) \to F (k) = G (k)$
9		climdm	$⊢ F \in dom ⇝ \leftrightarrow F ⇝ ⇝ (F)$
10	9	bilani	$⊢ (φ \land F \in dom ⇝) \to F ⇝ ⇝ (F)$
11	10 9	sylibr	$⊢ (φ \land F \in dom ⇝) \to F \in dom ⇝$
12		nfcv	$⊢ \underline{Ⅎ} k j$
13	12	nfel1	$⊢ Ⅎ k j \in Z$
14	1 13	nfan	$⊢ Ⅎ k (φ \land j \in Z)$
15	2 12	nffv	$⊢ \underline{Ⅎ} k F (j)$
16	3 12	nffv	$⊢ \underline{Ⅎ} k G (j)$
17	15 16	nfeq	$⊢ Ⅎ k F (j) = G (j)$
18	14 17	nfim	$⊢ Ⅎ k ((φ \land j \in Z) \to F (j) = G (j))$
19		eleq1w	$⊢ k = j \to (k \in Z \leftrightarrow j \in Z)$
20	19	anbi2d	$⊢ k = j \to ((φ \land k \in Z) \leftrightarrow (φ \land j \in Z))$
21		fveq2	$⊢ k = j \to F (k) = F (j)$
22		fveq2	$⊢ k = j \to G (k) = G (j)$
23	21 22	eqeq12d	$⊢ k = j \to (F (k) = G (k) \leftrightarrow F (j) = G (j))$
24	20 23	imbi12d	$⊢ k = j \to (((φ \land k \in Z) \to F (k) = G (k)) \leftrightarrow ((φ \land j \in Z) \to F (j) = G (j)))$
25	18 24 8	chvarfv	$⊢ (φ \land j \in Z) \to F (j) = G (j)$
26	4 5 6 7 25	climeldmeq	$⊢ φ \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$
27	26	adantr	$⊢ (φ \land F \in dom ⇝) \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$
28	11 27	mpbid	$⊢ (φ \land F \in dom ⇝) \to G \in dom ⇝$
29		climdm	$⊢ G \in dom ⇝ \leftrightarrow G ⇝ ⇝ (G)$
30	28 29	sylib	$⊢ (φ \land F \in dom ⇝) \to G ⇝ ⇝ (G)$
31	6	adantr	$⊢ (φ \land F \in dom ⇝) \to G \in W$
32	5	adantr	$⊢ (φ \land F \in dom ⇝) \to F \in V$
33	7	adantr	$⊢ (φ \land F \in dom ⇝) \to M \in ℤ$
34	25	eqcomd	$⊢ (φ \land j \in Z) \to G (j) = F (j)$
35	34	adantlr	$⊢ ((φ \land F \in dom ⇝) \land j \in Z) \to G (j) = F (j)$
36	4 31 32 33 35	climeq	$⊢ (φ \land F \in dom ⇝) \to (G ⇝ ⇝ (G) \leftrightarrow F ⇝ ⇝ (G))$
37	30 36	mpbid	$⊢ (φ \land F \in dom ⇝) \to F ⇝ ⇝ (G)$
38		climuni	$⊢ (F ⇝ ⇝ (F) \land F ⇝ ⇝ (G)) \to ⇝ (F) = ⇝ (G)$
39	10 37 38	syl2anc	$⊢ (φ \land F \in dom ⇝) \to ⇝ (F) = ⇝ (G)$
40		ndmfv	$⊢ \neg F \in dom ⇝ \to ⇝ (F) = \emptyset$
41	40	adantl	$⊢ (φ \land \neg F \in dom ⇝) \to ⇝ (F) = \emptyset$
42		simpr	$⊢ (φ \land \neg F \in dom ⇝) \to \neg F \in dom ⇝$
43	26	adantr	$⊢ (φ \land \neg F \in dom ⇝) \to (F \in dom ⇝ \leftrightarrow G \in dom ⇝)$
44	42 43	mtbid	$⊢ (φ \land \neg F \in dom ⇝) \to \neg G \in dom ⇝$
45		ndmfv	$⊢ \neg G \in dom ⇝ \to ⇝ (G) = \emptyset$
46	44 45	syl	$⊢ (φ \land \neg F \in dom ⇝) \to ⇝ (G) = \emptyset$
47	41 46	eqtr4d	$⊢ (φ \land \neg F \in dom ⇝) \to ⇝ (F) = ⇝ (G)$
48	39 47	pm2.61dan	$⊢ φ \to ⇝ (F) = ⇝ (G)$

Metamath Proof Explorer

Theorem climfveqf

Proof