Theorem climfveqmpt2

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

	Ref	Expression
Hypotheses	climfveqmpt2.k	⊢ Ⅎ 𝑘 𝜑
	climfveqmpt2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climfveqmpt2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climfveqmpt2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	climfveqmpt2.c	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	climfveqmpt2.s	⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
	climfveqmpt2.i	⊢ ( 𝜑 → 𝑍 ⊆ 𝐵 )
	climfveqmpt2.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ 𝑈 )
Assertion	climfveqmpt2	⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( ⇝ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		climfveqmpt2.k	⊢ Ⅎ 𝑘 𝜑
2		climfveqmpt2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climfveqmpt2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		climfveqmpt2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		climfveqmpt2.c	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
6		climfveqmpt2.s	⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
7		climfveqmpt2.i	⊢ ( 𝜑 → 𝑍 ⊆ 𝐵 )
8		climfveqmpt2.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ 𝑈 )
9		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
10		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐵 ↦ 𝐶 )
11	4	mptexd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∈ V )
12	5	mptexd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ∈ V )
13	6	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝐴 )
14		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
15	14	fvmpt2	⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
16	13 8 15	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
17	7	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝐵 )
18		eqid	⊢ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐵 ↦ 𝐶 )
19	18	fvmpt2	⊢ ( ( 𝑘 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
20	17 8 19	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
21	16 20	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) )
22	1 9 10 3 11 12 2 21	climfveqf	⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ) = ( ⇝ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )