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

Metamath Proof Explorer

Theorem climfveqf

Proof