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	$⊢ Ⅎ j φ$
	liminfequzmpt2.o	$⊢ \underline{Ⅎ} j A$
	liminfequzmpt2.p	$⊢ \underline{Ⅎ} j B$
	liminfequzmpt2.a	$⊢ A = ℤ_{\geq M}$
	liminfequzmpt2.b	$⊢ B = ℤ_{\geq N}$
	liminfequzmpt2.k	$⊢ φ \to K \in A$
	liminfequzmpt2.e	$⊢ φ \to K \in B$
	liminfequzmpt2.c	$⊢ (φ \land j \in ℤ_{\geq K}) \to C \in V$
Assertion	liminfequzmpt2	$⊢ φ \to lim inf ((j \in A ⟼ C)) = lim inf ((j \in B ⟼ C))$

Proof

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

Metamath Proof Explorer

Theorem liminfequzmpt2

Proof