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

Proof

Step	Hyp	Ref	Expression
1		climfveqmpt3.k	⊢ Ⅎ 𝑘 𝜑
2		climfveqmpt3.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climfveqmpt3.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		climfveqmpt3.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		climfveqmpt3.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6		climfveqmpt3.i	⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
7		climfveqmpt3.s	⊢ ( 𝜑 → 𝑍 ⊆ 𝐶 )
8		climfveqmpt3.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ 𝑈 )
9		climfveqmpt3.d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 = 𝐷 )
10	4	mptexd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
11	5	mptexd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ∈ V )
12		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
13	1 12	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
14		nfcv	⊢ Ⅎ 𝑘 𝑗
15	14	nfcsb1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
16	14	nfcsb1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐷
17	15 16	nfeq	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷
18	13 17	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
19		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
20	19	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
21		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
22		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐷 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
23	21 22	eqeq12d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 = 𝐷 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ) )
24	20 23	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 = 𝐷 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ) ) )
25	18 24 9	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
26	6	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑍 ⊆ 𝐴 )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
28	26 27	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝐴 )
29		nfcv	⊢ Ⅎ 𝑘 𝑈
30	15 29	nfel	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈
31	13 30	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈 )
32	21	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ 𝑈 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈 ) )
33	20 32	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ 𝑈 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈 ) ) )
34	31 33 8	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈 )
35		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
36	14 15 21 35	fvmptf	⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
37	28 34 36	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
38	7	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑍 ⊆ 𝐶 )
39	38 27	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝐶 )
40	25 34	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑈 )
41		eqid	⊢ ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) = ( 𝑘 ∈ 𝐶 ↦ 𝐷 )
42	14 16 22 41	fvmptf	⊢ ( ( 𝑗 ∈ 𝐶 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑈 ) → ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
43	39 40 42	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
44	25 37 43	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) )
45	3 10 11 2 44	climfveq	⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ⇝ ‘ ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ) )