climfveqmpt

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

	Ref	Expression
Hypotheses	climfveqmpt.k	$⊢ Ⅎ k φ$
	climfveqmpt.m	$⊢ φ \to M \in ℤ$
	climfveqmpt.z	$⊢ Z = ℤ_{\geq M}$
	climfveqmpt.A	$⊢ φ \to A \in R$
	climfveqmpt.i	$⊢ φ \to Z \subseteq A$
	climfveqmpt.b	$⊢ (φ \land k \in A) \to B \in V$
	climfveqmpt.t	$⊢ φ \to C \in S$
	climfveqmpt.l	$⊢ φ \to Z \subseteq C$
	climfveqmpt.c	$⊢ (φ \land k \in C) \to D \in W$
	climfveqmpt.e	$⊢ (φ \land k \in Z) \to B = D$
Assertion	climfveqmpt	$⊢ φ \to ⇝ ((k \in A ⟼ B)) = ⇝ ((k \in C ⟼ D))$

Proof

Step	Hyp	Ref	Expression
1		climfveqmpt.k	$⊢ Ⅎ k φ$
2		climfveqmpt.m	$⊢ φ \to M \in ℤ$
3		climfveqmpt.z	$⊢ Z = ℤ_{\geq M}$
4		climfveqmpt.A	$⊢ φ \to A \in R$
5		climfveqmpt.i	$⊢ φ \to Z \subseteq A$
6		climfveqmpt.b	$⊢ (φ \land k \in A) \to B \in V$
7		climfveqmpt.t	$⊢ φ \to C \in S$
8		climfveqmpt.l	$⊢ φ \to Z \subseteq C$
9		climfveqmpt.c	$⊢ (φ \land k \in C) \to D \in W$
10		climfveqmpt.e	$⊢ (φ \land k \in Z) \to B = D$
11	4	mptexd	$⊢ φ \to (k \in A ⟼ B) \in V$
12	7	mptexd	$⊢ φ \to (k \in C ⟼ D) \in V$
13		nfv	$⊢ Ⅎ k j \in Z$
14	1 13	nfan	$⊢ Ⅎ k (φ \land j \in Z)$
15		nfcv	$⊢ \underline{Ⅎ} k j$
16	15	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
17	15	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ D$
18	16 17	nfeq	$⊢ Ⅎ k ⦋ j / k ⦌ B = ⦋ j / k ⦌ D$
19	14 18	nfim	$⊢ Ⅎ k ((φ \land j \in Z) \to ⦋ j / k ⦌ B = ⦋ j / k ⦌ D)$
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		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
23		csbeq1a	$⊢ k = j \to D = ⦋ j / k ⦌ D$
24	22 23	eqeq12d	$⊢ k = j \to (B = D \leftrightarrow ⦋ j / k ⦌ B = ⦋ j / k ⦌ D)$
25	21 24	imbi12d	$⊢ k = j \to (((φ \land k \in Z) \to B = D) \leftrightarrow ((φ \land j \in Z) \to ⦋ j / k ⦌ B = ⦋ j / k ⦌ D))$
26	19 25 10	chvarfv	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ B = ⦋ j / k ⦌ D$
27	5	adantr	$⊢ (φ \land j \in Z) \to Z \subseteq A$
28		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
29	27 28	sseldd	$⊢ (φ \land j \in Z) \to j \in A$
30		simpr	$⊢ (φ \land j \in A) \to j \in A$
31		nfv	$⊢ Ⅎ k j \in A$
32	1 31	nfan	$⊢ Ⅎ k (φ \land j \in A)$
33		nfcv	$⊢ \underline{Ⅎ} k V$
34	16 33	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ B \in V$
35	32 34	nfim	$⊢ Ⅎ k ((φ \land j \in A) \to ⦋ j / k ⦌ B \in V)$
36		eleq1w	$⊢ k = j \to (k \in A \leftrightarrow j \in A)$
37	36	anbi2d	$⊢ k = j \to ((φ \land k \in A) \leftrightarrow (φ \land j \in A))$
38	22	eleq1d	$⊢ k = j \to (B \in V \leftrightarrow ⦋ j / k ⦌ B \in V)$
39	37 38	imbi12d	$⊢ k = j \to (((φ \land k \in A) \to B \in V) \leftrightarrow ((φ \land j \in A) \to ⦋ j / k ⦌ B \in V))$
40	35 39 6	chvarfv	$⊢ (φ \land j \in A) \to ⦋ j / k ⦌ B \in V$
41		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
42	15 16 22 41	fvmptf	$⊢ (j \in A \land ⦋ j / k ⦌ B \in V) \to (k \in A ⟼ B) (j) = ⦋ j / k ⦌ B$
43	30 40 42	syl2anc	$⊢ (φ \land j \in A) \to (k \in A ⟼ B) (j) = ⦋ j / k ⦌ B$
44	29 43	syldan	$⊢ (φ \land j \in Z) \to (k \in A ⟼ B) (j) = ⦋ j / k ⦌ B$
45	8	adantr	$⊢ (φ \land j \in Z) \to Z \subseteq C$
46	45 28	sseldd	$⊢ (φ \land j \in Z) \to j \in C$
47		simpr	$⊢ (φ \land j \in C) \to j \in C$
48		nfv	$⊢ Ⅎ k j \in C$
49	1 48	nfan	$⊢ Ⅎ k (φ \land j \in C)$
50		nfcv	$⊢ \underline{Ⅎ} k W$
51	17 50	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ D \in W$
52	49 51	nfim	$⊢ Ⅎ k ((φ \land j \in C) \to ⦋ j / k ⦌ D \in W)$
53		eleq1w	$⊢ k = j \to (k \in C \leftrightarrow j \in C)$
54	53	anbi2d	$⊢ k = j \to ((φ \land k \in C) \leftrightarrow (φ \land j \in C))$
55	23	eleq1d	$⊢ k = j \to (D \in W \leftrightarrow ⦋ j / k ⦌ D \in W)$
56	54 55	imbi12d	$⊢ k = j \to (((φ \land k \in C) \to D \in W) \leftrightarrow ((φ \land j \in C) \to ⦋ j / k ⦌ D \in W))$
57	52 56 9	chvarfv	$⊢ (φ \land j \in C) \to ⦋ j / k ⦌ D \in W$
58		eqid	$⊢ (k \in C ⟼ D) = (k \in C ⟼ D)$
59	15 17 23 58	fvmptf	$⊢ (j \in C \land ⦋ j / k ⦌ D \in W) \to (k \in C ⟼ D) (j) = ⦋ j / k ⦌ D$
60	47 57 59	syl2anc	$⊢ (φ \land j \in C) \to (k \in C ⟼ D) (j) = ⦋ j / k ⦌ D$
61	46 60	syldan	$⊢ (φ \land j \in Z) \to (k \in C ⟼ D) (j) = ⦋ j / k ⦌ D$
62	26 44 61	3eqtr4d	$⊢ (φ \land j \in Z) \to (k \in A ⟼ B) (j) = (k \in C ⟼ D) (j)$
63	3 11 12 2 62	climfveq	$⊢ φ \to ⇝ ((k \in A ⟼ B)) = ⇝ ((k \in C ⟼ D))$

Metamath Proof Explorer

Theorem climfveqmpt

Proof