climeqmpt

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

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

Step	Hyp	Ref	Expression
1		climeqmpt.x	$⊢ Ⅎ x φ$
2		climeqmpt.a	$⊢ φ \to A \in V$
3		climeqmpt.b	$⊢ φ \to B \in W$
4		climeqmpt.m	$⊢ φ \to M \in ℤ$
5		climeqmpt.z	$⊢ Z = ℤ_{\geq M}$
6		climeqmpt.s	$⊢ φ \to Z \subseteq A$
7		climeqmpt.t	$⊢ φ \to Z \subseteq B$
8		climeqmpt.c	$⊢ (φ \land x \in Z) \to C \in U$
9		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ C)$
10		nfmpt1	$⊢ \underline{Ⅎ} x (x \in B ⟼ C)$
11	2	mptexd	$⊢ φ \to (x \in A ⟼ C) \in V$
12	3	mptexd	$⊢ φ \to (x \in B ⟼ C) \in V$
13	6	adantr	$⊢ (φ \land x \in Z) \to Z \subseteq A$
14		simpr	$⊢ (φ \land x \in Z) \to x \in Z$
15	13 14	sseldd	$⊢ (φ \land x \in Z) \to x \in A$
16		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
17	16	fvmpt2	$⊢ (x \in A \land C \in U) \to (x \in A ⟼ C) (x) = C$
18	15 8 17	syl2anc	$⊢ (φ \land x \in Z) \to (x \in A ⟼ C) (x) = C$
19	7	adantr	$⊢ (φ \land x \in Z) \to Z \subseteq B$
20	19 14	sseldd	$⊢ (φ \land x \in Z) \to x \in B$
21		eqid	$⊢ (x \in B ⟼ C) = (x \in B ⟼ C)$
22	21	fvmpt2	$⊢ (x \in B \land C \in U) \to (x \in B ⟼ C) (x) = C$
23	20 8 22	syl2anc	$⊢ (φ \land x \in Z) \to (x \in B ⟼ C) (x) = C$
24	23	eqcomd	$⊢ (φ \land x \in Z) \to C = (x \in B ⟼ C) (x)$
25	18 24	eqtrd	$⊢ (φ \land x \in Z) \to (x \in A ⟼ C) (x) = (x \in B ⟼ C) (x)$
26	1 9 10 4 5 11 12 25	climeqf	$⊢ φ \to ((x \in A ⟼ C) ⇝ D \leftrightarrow (x \in B ⟼ C) ⇝ D)$

Metamath Proof Explorer