climfveqmpt3

Description: Two functions that are eventually equal to one another have the same limit. TODO: this is more general than climfveqmpt and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	climfveqmpt3.k	$⊢ Ⅎ k φ$
	climfveqmpt3.m	$⊢ φ \to M \in ℤ$
	climfveqmpt3.z	$⊢ Z = ℤ_{\geq M}$
	climfveqmpt3.a	$⊢ φ \to A \in V$
	climfveqmpt3.c	$⊢ φ \to C \in W$
	climfveqmpt3.i	$⊢ φ \to Z \subseteq A$
	climfveqmpt3.s	$⊢ φ \to Z \subseteq C$
	climfveqmpt3.b	$⊢ (φ \land k \in Z) \to B \in U$
	climfveqmpt3.d	$⊢ (φ \land k \in Z) \to B = D$
Assertion	climfveqmpt3	$⊢ φ \to ⇝ ((k \in A ⟼ B)) = ⇝ ((k \in C ⟼ D))$

Proof

Step	Hyp	Ref	Expression
1		climfveqmpt3.k	$⊢ Ⅎ k φ$
2		climfveqmpt3.m	$⊢ φ \to M \in ℤ$
3		climfveqmpt3.z	$⊢ Z = ℤ_{\geq M}$
4		climfveqmpt3.a	$⊢ φ \to A \in V$
5		climfveqmpt3.c	$⊢ φ \to C \in W$
6		climfveqmpt3.i	$⊢ φ \to Z \subseteq A$
7		climfveqmpt3.s	$⊢ φ \to Z \subseteq C$
8		climfveqmpt3.b	$⊢ (φ \land k \in Z) \to B \in U$
9		climfveqmpt3.d	$⊢ (φ \land k \in Z) \to B = D$
10	4	mptexd	$⊢ φ \to (k \in A ⟼ B) \in V$
11	5	mptexd	$⊢ φ \to (k \in C ⟼ D) \in V$
12		nfv	$⊢ Ⅎ k j \in Z$
13	1 12	nfan	$⊢ Ⅎ k (φ \land j \in Z)$
14		nfcv	$⊢ \underline{Ⅎ} k j$
15	14	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
16	14	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ D$
17	15 16	nfeq	$⊢ Ⅎ k ⦋ j / k ⦌ B = ⦋ j / k ⦌ D$
18	13 17	nfim	$⊢ Ⅎ k ((φ \land j \in Z) \to ⦋ j / k ⦌ B = ⦋ j / k ⦌ D)$
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		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
22		csbeq1a	$⊢ k = j \to D = ⦋ j / k ⦌ D$
23	21 22	eqeq12d	$⊢ k = j \to (B = D \leftrightarrow ⦋ j / k ⦌ B = ⦋ j / k ⦌ D)$
24	20 23	imbi12d	$⊢ k = j \to (((φ \land k \in Z) \to B = D) \leftrightarrow ((φ \land j \in Z) \to ⦋ j / k ⦌ B = ⦋ j / k ⦌ D))$
25	18 24 9	chvarfv	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ B = ⦋ j / k ⦌ D$
26	6	adantr	$⊢ (φ \land j \in Z) \to Z \subseteq A$
27		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
28	26 27	sseldd	$⊢ (φ \land j \in Z) \to j \in A$
29		nfcv	$⊢ \underline{Ⅎ} k U$
30	15 29	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ B \in U$
31	13 30	nfim	$⊢ Ⅎ k ((φ \land j \in Z) \to ⦋ j / k ⦌ B \in U)$
32	21	eleq1d	$⊢ k = j \to (B \in U \leftrightarrow ⦋ j / k ⦌ B \in U)$
33	20 32	imbi12d	$⊢ k = j \to (((φ \land k \in Z) \to B \in U) \leftrightarrow ((φ \land j \in Z) \to ⦋ j / k ⦌ B \in U))$
34	31 33 8	chvarfv	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ B \in U$
35		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
36	14 15 21 35	fvmptf	$⊢ (j \in A \land ⦋ j / k ⦌ B \in U) \to (k \in A ⟼ B) (j) = ⦋ j / k ⦌ B$
37	28 34 36	syl2anc	$⊢ (φ \land j \in Z) \to (k \in A ⟼ B) (j) = ⦋ j / k ⦌ B$
38	7	adantr	$⊢ (φ \land j \in Z) \to Z \subseteq C$
39	38 27	sseldd	$⊢ (φ \land j \in Z) \to j \in C$
40	25 34	eqeltrrd	$⊢ (φ \land j \in Z) \to ⦋ j / k ⦌ D \in U$
41		eqid	$⊢ (k \in C ⟼ D) = (k \in C ⟼ D)$
42	14 16 22 41	fvmptf	$⊢ (j \in C \land ⦋ j / k ⦌ D \in U) \to (k \in C ⟼ D) (j) = ⦋ j / k ⦌ D$
43	39 40 42	syl2anc	$⊢ (φ \land j \in Z) \to (k \in C ⟼ D) (j) = ⦋ j / k ⦌ D$
44	25 37 43	3eqtr4d	$⊢ (φ \land j \in Z) \to (k \in A ⟼ B) (j) = (k \in C ⟼ D) (j)$
45	3 10 11 2 44	climfveq	$⊢ φ \to ⇝ ((k \in A ⟼ B)) = ⇝ ((k \in C ⟼ D))$

Metamath Proof Explorer

Theorem climfveqmpt3

Proof