Theorem climeldmeqmpt2

Description: Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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