limsupequzmptlem

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

	Ref	Expression
Hypotheses	limsupequzmptlem.j	⊢ Ⅎ 𝑗 𝜑
	limsupequzmptlem.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	limsupequzmptlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	limsupequzmptlem.a	⊢ 𝐴 = ( ℤ_≥ ‘ 𝑀 )
	limsupequzmptlem.b	⊢ 𝐵 = ( ℤ_≥ ‘ 𝑁 )
	limsupequzmptlem.c	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
	limsupequzmptlem.d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ 𝑊 )
	limsupequzmptlem.k	⊢ 𝐾 = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 )
Assertion	limsupequzmptlem	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupequzmptlem.j	⊢ Ⅎ 𝑗 𝜑
2		limsupequzmptlem.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		limsupequzmptlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		limsupequzmptlem.a	⊢ 𝐴 = ( ℤ_≥ ‘ 𝑀 )
5		limsupequzmptlem.b	⊢ 𝐵 = ( ℤ_≥ ‘ 𝑁 )
6		limsupequzmptlem.c	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
7		limsupequzmptlem.d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ 𝑊 )
8		limsupequzmptlem.k	⊢ 𝐾 = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 )
9		nfmpt1	⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝐴 ↦ 𝐶 )
10		nfmpt1	⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝐵 ↦ 𝐶 )
11	4	eqcomi	⊢ ( ℤ_≥ ‘ 𝑀 ) = 𝐴
12	11	eleq2i	⊢ ( 𝑗 ∈ ( ℤ_≥ ‘ 𝑀 ) ↔ 𝑗 ∈ 𝐴 )
13	12	biimpi	⊢ ( 𝑗 ∈ ( ℤ_≥ ‘ 𝑀 ) → 𝑗 ∈ 𝐴 )
14	13 6	sylan2	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝑀 ) ) → 𝐶 ∈ 𝑉 )
15	4	mpteq1i	⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑗 ∈ ( ℤ_≥ ‘ 𝑀 ) ↦ 𝐶 )
16	1 14 15	fnmptd	⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) Fn ( ℤ_≥ ‘ 𝑀 ) )
17	5	eleq2i	⊢ ( 𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ( ℤ_≥ ‘ 𝑁 ) )
18	17	bicomi	⊢ ( 𝑗 ∈ ( ℤ_≥ ‘ 𝑁 ) ↔ 𝑗 ∈ 𝐵 )
19	18	biimpi	⊢ ( 𝑗 ∈ ( ℤ_≥ ‘ 𝑁 ) → 𝑗 ∈ 𝐵 )
20	19 7	sylan2	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝑁 ) ) → 𝐶 ∈ 𝑊 )
21	5	mpteq1i	⊢ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ ( ℤ_≥ ‘ 𝑁 ) ↦ 𝐶 )
22	1 20 21	fnmptd	⊢ ( 𝜑 → ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) Fn ( ℤ_≥ ‘ 𝑁 ) )
23	3 2	ifcld	⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ )
24	8 23	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
25		eqid	⊢ ( ℤ_≥ ‘ 𝑀 ) = ( ℤ_≥ ‘ 𝑀 )
26	2	zred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
27	3	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
28		max1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
29	26 27 28	syl2anc	⊢ ( 𝜑 → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
30	29 8	breqtrrdi	⊢ ( 𝜑 → 𝑀 ≤ 𝐾 )
31	25 2 24 30	eluzd	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ_≥ ‘ 𝑀 ) )
32	31	uzssd	⊢ ( 𝜑 → ( ℤ_≥ ‘ 𝐾 ) ⊆ ( ℤ_≥ ‘ 𝑀 ) )
33	11	a1i	⊢ ( 𝜑 → ( ℤ_≥ ‘ 𝑀 ) = 𝐴 )
34	32 33	sseqtrd	⊢ ( 𝜑 → ( ℤ_≥ ‘ 𝐾 ) ⊆ 𝐴 )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝐾 ) ) → ( ℤ_≥ ‘ 𝐾 ) ⊆ 𝐴 )
36		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝐾 ) ) → 𝑗 ∈ ( ℤ_≥ ‘ 𝐾 ) )
37	35 36	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝐾 ) ) → 𝑗 ∈ 𝐴 )
38	37 6	syldan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝐾 ) ) → 𝐶 ∈ 𝑉 )
39		eqid	⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑗 ∈ 𝐴 ↦ 𝐶 )
40	39	fvmpt2	⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑗 ) = 𝐶 )
41	37 38 40	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝐾 ) ) → ( ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑗 ) = 𝐶 )
42		eqid	⊢ ( ℤ_≥ ‘ 𝑁 ) = ( ℤ_≥ ‘ 𝑁 )
43		max2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
44	26 27 43	syl2anc	⊢ ( 𝜑 → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
45	44 8	breqtrrdi	⊢ ( 𝜑 → 𝑁 ≤ 𝐾 )
46	42 3 24 45	eluzd	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ_≥ ‘ 𝑁 ) )
47	46	uzssd	⊢ ( 𝜑 → ( ℤ_≥ ‘ 𝐾 ) ⊆ ( ℤ_≥ ‘ 𝑁 ) )
48	5	eqcomi	⊢ ( ℤ_≥ ‘ 𝑁 ) = 𝐵
49	48	a1i	⊢ ( 𝜑 → ( ℤ_≥ ‘ 𝑁 ) = 𝐵 )
50	47 49	sseqtrd	⊢ ( 𝜑 → ( ℤ_≥ ‘ 𝐾 ) ⊆ 𝐵 )
51	50	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝐾 ) ) → ( ℤ_≥ ‘ 𝐾 ) ⊆ 𝐵 )
52	51 36	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝐾 ) ) → 𝑗 ∈ 𝐵 )
53		eqid	⊢ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ 𝐵 ↦ 𝐶 )
54	53	fvmpt2	⊢ ( ( 𝑗 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑗 ) = 𝐶 )
55	52 38 54	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝐾 ) ) → ( ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑗 ) = 𝐶 )
56	41 55	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ_≥ ‘ 𝐾 ) ) → ( ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑗 ) = ( ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑗 ) )
57	1 9 10 2 16 3 22 24 56	limsupequz	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )

Metamath Proof Explorer

Theorem limsupequzmptlem

Proof