Theorem 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	⊢ Ⅎ 𝑘 𝜑
	climfveqmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climfveqmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climfveqmpt.A	⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
	climfveqmpt.i	⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
	climfveqmpt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	climfveqmpt.t	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
	climfveqmpt.l	⊢ ( 𝜑 → 𝑍 ⊆ 𝐶 )
	climfveqmpt.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐷 ∈ 𝑊 )
	climfveqmpt.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 = 𝐷 )
Assertion	climfveqmpt	⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ⇝ ‘ ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		climfveqmpt.k	⊢ Ⅎ 𝑘 𝜑
2		climfveqmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climfveqmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		climfveqmpt.A	⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
5		climfveqmpt.i	⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
6		climfveqmpt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
7		climfveqmpt.t	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
8		climfveqmpt.l	⊢ ( 𝜑 → 𝑍 ⊆ 𝐶 )
9		climfveqmpt.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐷 ∈ 𝑊 )
10		climfveqmpt.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 = 𝐷 )
11	4	mptexd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
12	7	mptexd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ∈ V )
13		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
14	1 13	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
15		nfcv	⊢ Ⅎ 𝑘 𝑗
16	15	nfcsb1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
17	15	nfcsb1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐷
18	16 17	nfeq	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷
19	14 18	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
20		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
21	20	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
22		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
23		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐷 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
24	22 23	eqeq12d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 = 𝐷 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ) )
25	21 24	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 = 𝐷 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ) ) )
26	19 25 10	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
27	5	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑍 ⊆ 𝐴 )
28		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
29	27 28	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝐴 )
30		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝐴 )
31		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝐴
32	1 31	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
33		nfcv	⊢ Ⅎ 𝑘 𝑉
34	16 33	nfel	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉
35	32 34	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 )
36		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
37	36	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ) )
38	22	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ 𝑉 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 ) )
39	37 38	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 ) ) )
40	35 39 6	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 )
41		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
42	15 16 22 41	fvmptf	⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑉 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
43	30 40 42	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
44	29 43	syldan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
45	8	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑍 ⊆ 𝐶 )
46	45 28	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝐶 )
47		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → 𝑗 ∈ 𝐶 )
48		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝐶
49	1 48	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐶 )
50		nfcv	⊢ Ⅎ 𝑘 𝑊
51	17 50	nfel	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊
52	49 51	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 )
53		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐶 ↔ 𝑗 ∈ 𝐶 ) )
54	53	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) ) )
55	23	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐷 ∈ 𝑊 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 ) )
56	54 55	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐷 ∈ 𝑊 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 ) ) )
57	52 56 9	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 )
58		eqid	⊢ ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) = ( 𝑘 ∈ 𝐶 ↦ 𝐷 )
59	15 17 23 58	fvmptf	⊢ ( ( 𝑗 ∈ 𝐶 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑊 ) → ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
60	47 57 59	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
61	46 60	syldan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
62	26 44 61	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) )
63	3 11 12 2 62	climfveq	⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ⇝ ‘ ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ) )