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	|- F/ k ph
	climeldmeqmpt2.m	|- ( ph -> M e. ZZ )
	climeldmeqmpt2.z	|- Z = ( ZZ>= ` M )
	climeldmeqmpt2.a	|- ( ph -> A e. W )
	climeldmeqmpt2.t	|- ( ph -> B e. V )
	climeldmeqmpt2.i	|- ( ph -> Z C_ A )
	climeldmeqmpt2.l	|- ( ph -> Z C_ B )
	climeldmeqmpt2.b	|- ( ( ph /\ k e. Z ) -> C e. U )
Assertion	climeldmeqmpt2	|- ( ph -> ( ( k e. A |-> C ) e. dom ~~> <-> ( k e. B |-> C ) e. dom ~~> ) )

Proof

Step	Hyp	Ref	Expression
1		climeldmeqmpt2.k	|- F/ k ph
2		climeldmeqmpt2.m	|- ( ph -> M e. ZZ )
3		climeldmeqmpt2.z	|- Z = ( ZZ>= ` M )
4		climeldmeqmpt2.a	|- ( ph -> A e. W )
5		climeldmeqmpt2.t	|- ( ph -> B e. V )
6		climeldmeqmpt2.i	|- ( ph -> Z C_ A )
7		climeldmeqmpt2.l	|- ( ph -> Z C_ B )
8		climeldmeqmpt2.b	|- ( ( ph /\ k e. Z ) -> C e. U )
9		nfmpt1	|- F/_ k ( k e. A |-> C )
10		nfmpt1	|- F/_ k ( k e. B |-> C )
11	4	mptexd	|- ( ph -> ( k e. A |-> C ) e. _V )
12	5	mptexd	|- ( ph -> ( k e. B |-> C ) e. _V )
13	6	sselda	|- ( ( ph /\ k e. Z ) -> k e. A )
14		fvmpt4	|- ( ( k e. A /\ C e. U ) -> ( ( k e. A |-> C ) ` k ) = C )
15	13 8 14	syl2anc	|- ( ( ph /\ k e. Z ) -> ( ( k e. A |-> C ) ` k ) = C )
16	7	sselda	|- ( ( ph /\ k e. Z ) -> k e. B )
17		fvmpt4	|- ( ( k e. B /\ C e. U ) -> ( ( k e. B |-> C ) ` k ) = C )
18	16 8 17	syl2anc	|- ( ( ph /\ k e. Z ) -> ( ( k e. B |-> C ) ` k ) = C )
19	15 18	eqtr4d	|- ( ( ph /\ k e. Z ) -> ( ( k e. A |-> C ) ` k ) = ( ( k e. B |-> C ) ` k ) )
20	1 9 10 3 11 12 2 19	climeldmeqf	|- ( ph -> ( ( k e. A |-> C ) e. dom ~~> <-> ( k e. B |-> C ) e. dom ~~> ) )