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	$⊢ Ⅎ j φ$
	limsupequzmptlem.m	$⊢ φ \to M \in ℤ$
	limsupequzmptlem.n	$⊢ φ \to N \in ℤ$
	limsupequzmptlem.a	$⊢ A = ℤ_{\geq M}$
	limsupequzmptlem.b	$⊢ B = ℤ_{\geq N}$
	limsupequzmptlem.c	$⊢ (φ \land j \in A) \to C \in V$
	limsupequzmptlem.d	$⊢ (φ \land j \in B) \to C \in W$
	limsupequzmptlem.k	$⊢ K = if (M \leq N, N, M)$
Assertion	limsupequzmptlem	$⊢ φ \to lim sup ((j \in A ⟼ C)) = lim sup ((j \in B ⟼ C))$

Proof

Step	Hyp	Ref	Expression
1		limsupequzmptlem.j	$⊢ Ⅎ j φ$
2		limsupequzmptlem.m	$⊢ φ \to M \in ℤ$
3		limsupequzmptlem.n	$⊢ φ \to N \in ℤ$
4		limsupequzmptlem.a	$⊢ A = ℤ_{\geq M}$
5		limsupequzmptlem.b	$⊢ B = ℤ_{\geq N}$
6		limsupequzmptlem.c	$⊢ (φ \land j \in A) \to C \in V$
7		limsupequzmptlem.d	$⊢ (φ \land j \in B) \to C \in W$
8		limsupequzmptlem.k	$⊢ K = if (M \leq N, N, M)$
9		nfmpt1	$⊢ \underline{Ⅎ} j (j \in A ⟼ C)$
10		nfmpt1	$⊢ \underline{Ⅎ} j (j \in B ⟼ C)$
11	4	eqcomi	$⊢ ℤ_{\geq M} = A$
12	11	eleq2i	$⊢ j \in ℤ_{\geq M} \leftrightarrow j \in A$
13	12	biimpi	$⊢ j \in ℤ_{\geq M} \to j \in A$
14	13 6	sylan2	$⊢ (φ \land j \in ℤ_{\geq M}) \to C \in V$
15	4	mpteq1i	$⊢ (j \in A ⟼ C) = (j \in ℤ_{\geq M} ⟼ C)$
16	1 14 15	fnmptd	$⊢ φ \to (j \in A ⟼ C) Fn ℤ_{\geq M}$
17	5	eleq2i	$⊢ j \in B \leftrightarrow j \in ℤ_{\geq N}$
18	17	bicomi	$⊢ j \in ℤ_{\geq N} \leftrightarrow j \in B$
19	18	biimpi	$⊢ j \in ℤ_{\geq N} \to j \in B$
20	19 7	sylan2	$⊢ (φ \land j \in ℤ_{\geq N}) \to C \in W$
21	5	mpteq1i	$⊢ (j \in B ⟼ C) = (j \in ℤ_{\geq N} ⟼ C)$
22	1 20 21	fnmptd	$⊢ φ \to (j \in B ⟼ C) Fn ℤ_{\geq N}$
23	3 2	ifcld	$⊢ φ \to if (M \leq N, N, M) \in ℤ$
24	8 23	eqeltrid	$⊢ φ \to K \in ℤ$
25		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
26	2	zred	$⊢ φ \to M \in ℝ$
27	3	zred	$⊢ φ \to N \in ℝ$
28		max1	$⊢ (M \in ℝ \land N \in ℝ) \to M \leq if (M \leq N, N, M)$
29	26 27 28	syl2anc	$⊢ φ \to M \leq if (M \leq N, N, M)$
30	29 8	breqtrrdi	$⊢ φ \to M \leq K$
31	25 2 24 30	eluzd	$⊢ φ \to K \in ℤ_{\geq M}$
32	31	uzssd	$⊢ φ \to ℤ_{\geq K} \subseteq ℤ_{\geq M}$
33	11	a1i	$⊢ φ \to ℤ_{\geq M} = A$
34	32 33	sseqtrd	$⊢ φ \to ℤ_{\geq K} \subseteq A$
35	34	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to ℤ_{\geq K} \subseteq A$
36		simpr	$⊢ (φ \land j \in ℤ_{\geq K}) \to j \in ℤ_{\geq K}$
37	35 36	sseldd	$⊢ (φ \land j \in ℤ_{\geq K}) \to j \in A$
38	37 6	syldan	$⊢ (φ \land j \in ℤ_{\geq K}) \to C \in V$
39		eqid	$⊢ (j \in A ⟼ C) = (j \in A ⟼ C)$
40	39	fvmpt2	$⊢ (j \in A \land C \in V) \to (j \in A ⟼ C) (j) = C$
41	37 38 40	syl2anc	$⊢ (φ \land j \in ℤ_{\geq K}) \to (j \in A ⟼ C) (j) = C$
42		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
43		max2	$⊢ (M \in ℝ \land N \in ℝ) \to N \leq if (M \leq N, N, M)$
44	26 27 43	syl2anc	$⊢ φ \to N \leq if (M \leq N, N, M)$
45	44 8	breqtrrdi	$⊢ φ \to N \leq K$
46	42 3 24 45	eluzd	$⊢ φ \to K \in ℤ_{\geq N}$
47	46	uzssd	$⊢ φ \to ℤ_{\geq K} \subseteq ℤ_{\geq N}$
48	5	eqcomi	$⊢ ℤ_{\geq N} = B$
49	48	a1i	$⊢ φ \to ℤ_{\geq N} = B$
50	47 49	sseqtrd	$⊢ φ \to ℤ_{\geq K} \subseteq B$
51	50	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to ℤ_{\geq K} \subseteq B$
52	51 36	sseldd	$⊢ (φ \land j \in ℤ_{\geq K}) \to j \in B$
53		eqid	$⊢ (j \in B ⟼ C) = (j \in B ⟼ C)$
54	53	fvmpt2	$⊢ (j \in B \land C \in V) \to (j \in B ⟼ C) (j) = C$
55	52 38 54	syl2anc	$⊢ (φ \land j \in ℤ_{\geq K}) \to (j \in B ⟼ C) (j) = C$
56	41 55	eqtr4d	$⊢ (φ \land j \in ℤ_{\geq K}) \to (j \in A ⟼ C) (j) = (j \in B ⟼ C) (j)$
57	1 9 10 2 16 3 22 24 56	limsupequz	$⊢ φ \to lim sup ((j \in A ⟼ C)) = lim sup ((j \in B ⟼ C))$

Metamath Proof Explorer

Theorem limsupequzmptlem

Proof