Theorem climeldmeqmpt3

Description: Two functions that are eventually equal, either both are convergent or both are divergent. TODO: this is more general than climeldmeqmpt and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		climeldmeqmpt3.k	⊢ Ⅎ 𝑘 𝜑
2		climeldmeqmpt3.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climeldmeqmpt3.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		climeldmeqmpt3.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		climeldmeqmpt3.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6		climeldmeqmpt3.i	⊢ ( 𝜑 → 𝑍 ⊆ 𝐴 )
7		climeldmeqmpt3.s	⊢ ( 𝜑 → 𝑍 ⊆ 𝐶 )
8		climeldmeqmpt3.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ 𝑈 )
9		climeldmeqmpt3.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 = 𝐷 )
10	4	mptexd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
11	5	mptexd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ∈ V )
12		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
13	1 12	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
14		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
15		nfcv	⊢ Ⅎ 𝑘 𝑗
16	15	nfcsb1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐷
17	14 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	sselda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝐴 )
27		nfcv	⊢ Ⅎ 𝑘 𝑈
28	14 27	nfel	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈
29	13 28	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈 )
30	21	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ 𝑈 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈 ) )
31	20 30	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ 𝑈 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈 ) ) )
32	29 31 8	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈 )
33	15	nfcsb1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
34		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
35	15 33 21 34	fvmptf	⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ 𝑈 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
36	26 32 35	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
37	7	sselda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝐶 )
38	25 32	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑈 )
39		eqid	⊢ ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) = ( 𝑘 ∈ 𝐶 ↦ 𝐷 )
40	15 16 22 39	fvmptf	⊢ ( ( 𝑗 ∈ 𝐶 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐷 ∈ 𝑈 ) → ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
41	37 38 40	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐷 )
42	25 36 41	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑗 ) = ( ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑗 ) )
43	3 10 11 2 42	climeldmeq	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ dom ⇝ ↔ ( 𝑘 ∈ 𝐶 ↦ 𝐷 ) ∈ dom ⇝ ) )