Theorem liminfequzmpt2

Description: Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfequzmpt2.j	|- F/ j ph
	liminfequzmpt2.o	|- F/_ j A
	liminfequzmpt2.p	|- F/_ j B
	liminfequzmpt2.a	|- A = ( ZZ>= ` M )
	liminfequzmpt2.b	|- B = ( ZZ>= ` N )
	liminfequzmpt2.k	|- ( ph -> K e. A )
	liminfequzmpt2.e	|- ( ph -> K e. B )
	liminfequzmpt2.c	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> C e. V )
Assertion	liminfequzmpt2	|- ( ph -> ( liminf ` ( j e. A |-> C ) ) = ( liminf ` ( j e. B |-> C ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfequzmpt2.j	|- F/ j ph
2		liminfequzmpt2.o	|- F/_ j A
3		liminfequzmpt2.p	|- F/_ j B
4		liminfequzmpt2.a	|- A = ( ZZ>= ` M )
5		liminfequzmpt2.b	|- B = ( ZZ>= ` N )
6		liminfequzmpt2.k	|- ( ph -> K e. A )
7		liminfequzmpt2.e	|- ( ph -> K e. B )
8		liminfequzmpt2.c	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> C e. V )
9	4 6	uzssd2	|- ( ph -> ( ZZ>= ` K ) C_ A )
10	9	adantr	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ZZ>= ` K ) C_ A )
11		simpr	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. ( ZZ>= ` K ) )
12	10 11	sseldd	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. A )
13	8	elexd	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> C e. _V )
14	12 13	jca	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( j e. A /\ C e. _V ) )
15		rabid	|- ( j e. { j e. A | C e. _V } <-> ( j e. A /\ C e. _V ) )
16	14 15	sylibr	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. { j e. A | C e. _V } )
17	16	ex	|- ( ph -> ( j e. ( ZZ>= ` K ) -> j e. { j e. A | C e. _V } ) )
18	1 17	ralrimi	|- ( ph -> A. j e. ( ZZ>= ` K ) j e. { j e. A | C e. _V } )
19		nfcv	|- F/_ j ( ZZ>= ` K )
20		nfrab1	|- F/_ j { j e. A | C e. _V }
21	19 20	dfss3f	|- ( ( ZZ>= ` K ) C_ { j e. A | C e. _V } <-> A. j e. ( ZZ>= ` K ) j e. { j e. A | C e. _V } )
22	18 21	sylibr	|- ( ph -> ( ZZ>= ` K ) C_ { j e. A | C e. _V } )
23	20 19	resmptf	|- ( ( ZZ>= ` K ) C_ { j e. A | C e. _V } -> ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) = ( j e. ( ZZ>= ` K ) |-> C ) )
24	22 23	syl	|- ( ph -> ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) = ( j e. ( ZZ>= ` K ) |-> C ) )
25	24	eqcomd	|- ( ph -> ( j e. ( ZZ>= ` K ) |-> C ) = ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) )
26	25	fveq2d	|- ( ph -> ( liminf ` ( j e. ( ZZ>= ` K ) |-> C ) ) = ( liminf ` ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) ) )
27	4 6	eluzelz2d	|- ( ph -> K e. ZZ )
28		eqid	|- ( ZZ>= ` K ) = ( ZZ>= ` K )
29	4	fvexi	|- A e. _V
30	2 29	rabexf	|- { j e. A | C e. _V } e. _V
31	20 30	mptexf	|- ( j e. { j e. A | C e. _V } |-> C ) e. _V
32	31	a1i	|- ( ph -> ( j e. { j e. A | C e. _V } |-> C ) e. _V )
33		eqid	|- ( j e. { j e. A | C e. _V } |-> C ) = ( j e. { j e. A | C e. _V } |-> C )
34	20 33	dmmptssf	|- dom ( j e. { j e. A | C e. _V } |-> C ) C_ { j e. A | C e. _V }
35	2	ssrab2f	|- { j e. A | C e. _V } C_ A
36		uzssz	|- ( ZZ>= ` M ) C_ ZZ
37	4 36	eqsstri	|- A C_ ZZ
38	35 37	sstri	|- { j e. A | C e. _V } C_ ZZ
39	34 38	sstri	|- dom ( j e. { j e. A | C e. _V } |-> C ) C_ ZZ
40	39	a1i	|- ( ph -> dom ( j e. { j e. A | C e. _V } |-> C ) C_ ZZ )
41	27 28 32 40	liminfresuz2	|- ( ph -> ( liminf ` ( ( j e. { j e. A | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) ) = ( liminf ` ( j e. { j e. A | C e. _V } |-> C ) ) )
42	26 41	eqtr2d	|- ( ph -> ( liminf ` ( j e. { j e. A | C e. _V } |-> C ) ) = ( liminf ` ( j e. ( ZZ>= ` K ) |-> C ) ) )
43	5 7	uzssd2	|- ( ph -> ( ZZ>= ` K ) C_ B )
44	43	adantr	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( ZZ>= ` K ) C_ B )
45	44 11	sseldd	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. B )
46	45 13	jca	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( j e. B /\ C e. _V ) )
47		rabid	|- ( j e. { j e. B | C e. _V } <-> ( j e. B /\ C e. _V ) )
48	46 47	sylibr	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> j e. { j e. B | C e. _V } )
49	48	ex	|- ( ph -> ( j e. ( ZZ>= ` K ) -> j e. { j e. B | C e. _V } ) )
50	1 49	ralrimi	|- ( ph -> A. j e. ( ZZ>= ` K ) j e. { j e. B | C e. _V } )
51		nfrab1	|- F/_ j { j e. B | C e. _V }
52	19 51	dfss3f	|- ( ( ZZ>= ` K ) C_ { j e. B | C e. _V } <-> A. j e. ( ZZ>= ` K ) j e. { j e. B | C e. _V } )
53	50 52	sylibr	|- ( ph -> ( ZZ>= ` K ) C_ { j e. B | C e. _V } )
54	51 19	resmptf	|- ( ( ZZ>= ` K ) C_ { j e. B | C e. _V } -> ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) = ( j e. ( ZZ>= ` K ) |-> C ) )
55	53 54	syl	|- ( ph -> ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) = ( j e. ( ZZ>= ` K ) |-> C ) )
56	55	eqcomd	|- ( ph -> ( j e. ( ZZ>= ` K ) |-> C ) = ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) )
57	56	fveq2d	|- ( ph -> ( liminf ` ( j e. ( ZZ>= ` K ) |-> C ) ) = ( liminf ` ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) ) )
58	5	fvexi	|- B e. _V
59	3 58	rabexf	|- { j e. B | C e. _V } e. _V
60	51 59	mptexf	|- ( j e. { j e. B | C e. _V } |-> C ) e. _V
61	60	a1i	|- ( ph -> ( j e. { j e. B | C e. _V } |-> C ) e. _V )
62		eqid	|- ( j e. { j e. B | C e. _V } |-> C ) = ( j e. { j e. B | C e. _V } |-> C )
63	51 62	dmmptssf	|- dom ( j e. { j e. B | C e. _V } |-> C ) C_ { j e. B | C e. _V }
64	3	ssrab2f	|- { j e. B | C e. _V } C_ B
65		uzssz	|- ( ZZ>= ` N ) C_ ZZ
66	5 65	eqsstri	|- B C_ ZZ
67	64 66	sstri	|- { j e. B | C e. _V } C_ ZZ
68	63 67	sstri	|- dom ( j e. { j e. B | C e. _V } |-> C ) C_ ZZ
69	68	a1i	|- ( ph -> dom ( j e. { j e. B | C e. _V } |-> C ) C_ ZZ )
70	27 28 61 69	liminfresuz2	|- ( ph -> ( liminf ` ( ( j e. { j e. B | C e. _V } |-> C ) |` ( ZZ>= ` K ) ) ) = ( liminf ` ( j e. { j e. B | C e. _V } |-> C ) ) )
71	57 70	eqtr2d	|- ( ph -> ( liminf ` ( j e. { j e. B | C e. _V } |-> C ) ) = ( liminf ` ( j e. ( ZZ>= ` K ) |-> C ) ) )
72	42 71	eqtr4d	|- ( ph -> ( liminf ` ( j e. { j e. A | C e. _V } |-> C ) ) = ( liminf ` ( j e. { j e. B | C e. _V } |-> C ) ) )
73		eqid	|- { j e. A | C e. _V } = { j e. A | C e. _V }
74	2 73	mptssid	|- ( j e. A |-> C ) = ( j e. { j e. A | C e. _V } |-> C )
75	74	fveq2i	|- ( liminf ` ( j e. A |-> C ) ) = ( liminf ` ( j e. { j e. A | C e. _V } |-> C ) )
76	75	a1i	|- ( ph -> ( liminf ` ( j e. A |-> C ) ) = ( liminf ` ( j e. { j e. A | C e. _V } |-> C ) ) )
77		eqid	|- { j e. B | C e. _V } = { j e. B | C e. _V }
78	3 77	mptssid	|- ( j e. B |-> C ) = ( j e. { j e. B | C e. _V } |-> C )
79	78	fveq2i	|- ( liminf ` ( j e. B |-> C ) ) = ( liminf ` ( j e. { j e. B | C e. _V } |-> C ) )
80	79	a1i	|- ( ph -> ( liminf ` ( j e. B |-> C ) ) = ( liminf ` ( j e. { j e. B | C e. _V } |-> C ) ) )
81	72 76 80	3eqtr4d	|- ( ph -> ( liminf ` ( j e. A |-> C ) ) = ( liminf ` ( j e. B |-> C ) ) )