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	⊢ Ⅎ 𝑥 𝜑
	climeqmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	climeqmpt.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	climeqmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climeqmpt.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	climeqmpt.s	⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
	climeqmpt.t	⊢ ( 𝜑 → 𝑍 ⊆ 𝐵 )
	climeqmpt.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐶 ∈ 𝑈 )
Assertion	climeqmpt	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝ 𝐷 ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ⇝ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		climeqmpt.x	⊢ Ⅎ 𝑥 𝜑
2		climeqmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		climeqmpt.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		climeqmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		climeqmpt.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
6		climeqmpt.s	⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
7		climeqmpt.t	⊢ ( 𝜑 → 𝑍 ⊆ 𝐵 )
8		climeqmpt.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐶 ∈ 𝑈 )
9		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
10		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
11	2	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ V )
12	3	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ V )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑍 ⊆ 𝐴 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∈ 𝑍 )
15	13 14	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∈ 𝐴 )
16		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
17	16	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
18	15 8 17	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
19	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑍 ⊆ 𝐵 )
20	19 14	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∈ 𝐵 )
21		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
22	21	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
23	20 8 22	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
24	23	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐶 = ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) )
25	18 24	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑥 ) )
26	1 9 10 4 5 11 12 25	climeqf	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝ 𝐷 ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ⇝ 𝐷 ) )

Metamath Proof Explorer

Theorem climeqmpt

Proof