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	⊢ Ⅎ 𝑗 𝜑
	liminfequzmpt2.o	⊢ Ⅎ 𝑗 𝐴
	liminfequzmpt2.p	⊢ Ⅎ 𝑗 𝐵
	liminfequzmpt2.a	⊢ 𝐴 = ( ℤ≥ ‘ 𝑀 )
	liminfequzmpt2.b	⊢ 𝐵 = ( ℤ≥ ‘ 𝑁 )
	liminfequzmpt2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐴 )
	liminfequzmpt2.e	⊢ ( 𝜑 → 𝐾 ∈ 𝐵 )
	liminfequzmpt2.c	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐶 ∈ 𝑉 )
Assertion	liminfequzmpt2	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfequzmpt2.j	⊢ Ⅎ 𝑗 𝜑
2		liminfequzmpt2.o	⊢ Ⅎ 𝑗 𝐴
3		liminfequzmpt2.p	⊢ Ⅎ 𝑗 𝐵
4		liminfequzmpt2.a	⊢ 𝐴 = ( ℤ≥ ‘ 𝑀 )
5		liminfequzmpt2.b	⊢ 𝐵 = ( ℤ≥ ‘ 𝑁 )
6		liminfequzmpt2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐴 )
7		liminfequzmpt2.e	⊢ ( 𝜑 → 𝐾 ∈ 𝐵 )
8		liminfequzmpt2.c	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐶 ∈ 𝑉 )
9	4 6	uzssd2	⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐴 )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐴 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) )
12	10 11	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ 𝐴 )
13	8	elexd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐶 ∈ V )
14	12 13	jca	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑗 ∈ 𝐴 ∧ 𝐶 ∈ V ) )
15		rabid	⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↔ ( 𝑗 ∈ 𝐴 ∧ 𝐶 ∈ V ) )
16	14 15	sylibr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } )
17	16	ex	⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ) )
18	1 17	ralrimi	⊢ ( 𝜑 → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } )
19		nfcv	⊢ Ⅎ 𝑗 ( ℤ≥ ‘ 𝐾 )
20		nfrab1	⊢ Ⅎ 𝑗 { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V }
21	19 20	dfss3f	⊢ ( ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } )
22	18 21	sylibr	⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } )
23	20 19	resmptf	⊢ ( ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } → ( ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) )
24	22 23	syl	⊢ ( 𝜑 → ( ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) )
25	24	eqcomd	⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) = ( ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) )
26	25	fveq2d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) ) = ( lim inf ‘ ( ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ) )
27	4 6	eluzelz2d	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
28		eqid	⊢ ( ℤ≥ ‘ 𝐾 ) = ( ℤ≥ ‘ 𝐾 )
29	4	fvexi	⊢ 𝐴 ∈ V
30	2 29	rabexf	⊢ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ∈ V
31	20 30	mptexf	⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ∈ V
32	31	a1i	⊢ ( 𝜑 → ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ∈ V )
33		eqid	⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) = ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 )
34	20 33	dmmptssf	⊢ dom ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V }
35	2	ssrab2f	⊢ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ⊆ 𝐴
36		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
37	4 36	eqsstri	⊢ 𝐴 ⊆ ℤ
38	35 37	sstri	⊢ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ⊆ ℤ
39	34 38	sstri	⊢ dom ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ ℤ
40	39	a1i	⊢ ( 𝜑 → dom ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ ℤ )
41	27 28 32 40	liminfresuz2	⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) )
42	26 41	eqtr2d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) ) )
43	5 7	uzssd2	⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐵 )
44	43	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐵 )
45	44 11	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ 𝐵 )
46	45 13	jca	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑗 ∈ 𝐵 ∧ 𝐶 ∈ V ) )
47		rabid	⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↔ ( 𝑗 ∈ 𝐵 ∧ 𝐶 ∈ V ) )
48	46 47	sylibr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } )
49	48	ex	⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ) )
50	1 49	ralrimi	⊢ ( 𝜑 → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } )
51		nfrab1	⊢ Ⅎ 𝑗 { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V }
52	19 51	dfss3f	⊢ ( ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } )
53	50 52	sylibr	⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } )
54	51 19	resmptf	⊢ ( ( ℤ≥ ‘ 𝐾 ) ⊆ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } → ( ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) )
55	53 54	syl	⊢ ( 𝜑 → ( ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) )
56	55	eqcomd	⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) = ( ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) )
57	56	fveq2d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) ) = ( lim inf ‘ ( ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ) )
58	5	fvexi	⊢ 𝐵 ∈ V
59	3 58	rabexf	⊢ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ∈ V
60	51 59	mptexf	⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ∈ V
61	60	a1i	⊢ ( 𝜑 → ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ∈ V )
62		eqid	⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) = ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 )
63	51 62	dmmptssf	⊢ dom ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V }
64	3	ssrab2f	⊢ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ⊆ 𝐵
65		uzssz	⊢ ( ℤ≥ ‘ 𝑁 ) ⊆ ℤ
66	5 65	eqsstri	⊢ 𝐵 ⊆ ℤ
67	64 66	sstri	⊢ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ⊆ ℤ
68	63 67	sstri	⊢ dom ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ ℤ
69	68	a1i	⊢ ( 𝜑 → dom ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ⊆ ℤ )
70	27 28 61 69	liminfresuz2	⊢ ( 𝜑 → ( lim inf ‘ ( ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ↾ ( ℤ≥ ‘ 𝐾 ) ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) )
71	57 70	eqtr2d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ↦ 𝐶 ) ) )
72	42 71	eqtr4d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) )
73		eqid	⊢ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } = { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V }
74	2 73	mptssid	⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 )
75	74	fveq2i	⊢ ( lim inf ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) )
76	75	a1i	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) )
77		eqid	⊢ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } = { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V }
78	3 77	mptssid	⊢ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 )
79	78	fveq2i	⊢ ( lim inf ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) )
80	79	a1i	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ { 𝑗 ∈ 𝐵 ∣ 𝐶 ∈ V } ↦ 𝐶 ) ) )
81	72 76 80	3eqtr4d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim inf ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )