smflimsuplem5

Description: H converges to the superior limit of F . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smflimsuplem5.a	$⊢ Ⅎ n φ$
	smflimsuplem5.b	$⊢ Ⅎ m φ$
	smflimsuplem5.m	$⊢ φ \to M \in ℤ$
	smflimsuplem5.z	$⊢ Z = ℤ_{\geq M}$
	smflimsuplem5.s	$⊢ φ \to S \in SAlg$
	smflimsuplem5.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflimsuplem5.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
	smflimsuplem5.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
	smflimsuplem5.r	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (X))) \in ℝ$
	smflimsuplem5.n	$⊢ φ \to N \in Z$
	smflimsuplem5.x	$⊢ φ \to X \in ⋂_{m \in ℤ_{\geq N}} dom F (m)$
Assertion	smflimsuplem5	$⊢ φ \to (n \in ℤ_{\geq N} ⟼ H (n) (X)) ⇝ lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X)))$

Proof

Step	Hyp	Ref	Expression
1		smflimsuplem5.a	$⊢ Ⅎ n φ$
2		smflimsuplem5.b	$⊢ Ⅎ m φ$
3		smflimsuplem5.m	$⊢ φ \to M \in ℤ$
4		smflimsuplem5.z	$⊢ Z = ℤ_{\geq M}$
5		smflimsuplem5.s	$⊢ φ \to S \in SAlg$
6		smflimsuplem5.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
7		smflimsuplem5.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
8		smflimsuplem5.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
9		smflimsuplem5.r	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (X))) \in ℝ$
10		smflimsuplem5.n	$⊢ φ \to N \in Z$
11		smflimsuplem5.x	$⊢ φ \to X \in ⋂_{m \in ℤ_{\geq N}} dom F (m)$
12	4	eleq2i	$⊢ N \in Z \leftrightarrow N \in ℤ_{\geq M}$
13	12	biimpi	$⊢ N \in Z \to N \in ℤ_{\geq M}$
14		uzss	$⊢ N \in ℤ_{\geq M} \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
15	13 14	syl	$⊢ N \in Z \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
16	15 4	sseqtrrdi	$⊢ N \in Z \to ℤ_{\geq N} \subseteq Z$
17	10 16	syl	$⊢ φ \to ℤ_{\geq N} \subseteq Z$
18	17	sselda	$⊢ (φ \land n \in ℤ_{\geq N}) \to n \in Z$
19		nfcv	$⊢ \underline{Ⅎ} x Z$
20		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
21	19 20	nfmpt	$⊢ \underline{Ⅎ} x (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
22	7 21	nfcxfr	$⊢ \underline{Ⅎ} x E$
23		nfcv	$⊢ \underline{Ⅎ} x n$
24	22 23	nffv	$⊢ \underline{Ⅎ} x E (n)$
25		fvex	$⊢ E (n) \in V$
26	24 25	mptexf	$⊢ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) \in V$
27	26	a1i	$⊢ (φ \land n \in ℤ_{\geq N}) \to (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) \in V$
28	8	fvmpt2	$⊢ (n \in Z \land (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) \in V) \to H (n) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <))$
29	18 27 28	syl2anc	$⊢ (φ \land n \in ℤ_{\geq N}) \to H (n) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <))$
30	29	fveq1d	$⊢ (φ \land n \in ℤ_{\geq N}) \to H (n) (X) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) (X)$
31		nfcv	$⊢ \underline{Ⅎ} y E (n)$
32		nfcv	$⊢ \underline{Ⅎ} y sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)$
33		nfcv	$⊢ \underline{Ⅎ} x sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{*} <)$
34		fveq2	$⊢ x = y \to F (m) (x) = F (m) (y)$
35	34	mpteq2dv	$⊢ x = y \to (m \in ℤ_{\geq n} ⟼ F (m) (x)) = (m \in ℤ_{\geq n} ⟼ F (m) (y))$
36	35	rneqd	$⊢ x = y \to ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) = ran (m \in ℤ_{\geq n} ⟼ F (m) (y))$
37	36	supeq1d	$⊢ x = y \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <)$
38	24 31 32 33 37	cbvmptf	$⊢ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) = (y \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <))$
39		simpl	$⊢ (y = X \land m \in ℤ_{\geq n}) \to y = X$
40	39	fveq2d	$⊢ (y = X \land m \in ℤ_{\geq n}) \to F (m) (y) = F (m) (X)$
41	40	mpteq2dva	$⊢ y = X \to (m \in ℤ_{\geq n} ⟼ F (m) (y)) = (m \in ℤ_{\geq n} ⟼ F (m) (X))$
42	41	rneqd	$⊢ y = X \to ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) = ran (m \in ℤ_{\geq n} ⟼ F (m) (X))$
43	42	supeq1d	$⊢ y = X \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{} <)$
44	43	eleq1d	$⊢ y = X \to (sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{} <) \in ℝ)$
45		uzss	$⊢ n \in ℤ_{\geq N} \to ℤ_{\geq n} \subseteq ℤ_{\geq N}$
46		iinss1	$⊢ ℤ_{\geq n} \subseteq ℤ_{\geq N} \to ⋂_{m \in ℤ_{\geq N}} dom F (m) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
47	45 46	syl	$⊢ n \in ℤ_{\geq N} \to ⋂_{m \in ℤ_{\geq N}} dom F (m) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
48	47	adantl	$⊢ (φ \land n \in ℤ_{\geq N}) \to ⋂_{m \in ℤ_{\geq N}} dom F (m) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
49	11	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to X \in ⋂_{m \in ℤ_{\geq N}} dom F (m)$
50	48 49	sseldd	$⊢ (φ \land n \in ℤ_{\geq N}) \to X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
51		nfv	$⊢ Ⅎ m n \in ℤ_{\geq N}$
52	2 51	nfan	$⊢ Ⅎ m (φ \land n \in ℤ_{\geq N})$
53		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
54		simpll	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in ℤ_{\geq n}) \to φ$
55	45	sselda	$⊢ (n \in ℤ_{\geq N} \land m \in ℤ_{\geq n}) \to m \in ℤ_{\geq N}$
56	55	adantll	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in ℤ_{\geq n}) \to m \in ℤ_{\geq N}$
57	5	adantr	$⊢ (φ \land m \in ℤ_{\geq N}) \to S \in SAlg$
58		simpl	$⊢ (φ \land m \in ℤ_{\geq N}) \to φ$
59	17	sselda	$⊢ (φ \land m \in ℤ_{\geq N}) \to m \in Z$
60	6	ffvelrnda	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
61	58 59 60	syl2anc	$⊢ (φ \land m \in ℤ_{\geq N}) \to F (m) \in SMblFn (S)$
62		eqid	$⊢ dom F (m) = dom F (m)$
63	57 61 62	smff	$⊢ (φ \land m \in ℤ_{\geq N}) \to F (m) : dom F (m) ⟶ ℝ$
64		eliin	$⊢ X \in ⋂_{m \in ℤ_{\geq N}} dom F (m) \to (X \in ⋂_{m \in ℤ_{\geq N}} dom F (m) \leftrightarrow \forall m \in ℤ_{\geq N} X \in dom F (m))$
65	11 64	syl	$⊢ φ \to (X \in ⋂_{m \in ℤ_{\geq N}} dom F (m) \leftrightarrow \forall m \in ℤ_{\geq N} X \in dom F (m))$
66	11 65	mpbid	$⊢ φ \to \forall m \in ℤ_{\geq N} X \in dom F (m)$
67	66	adantr	$⊢ (φ \land m \in ℤ_{\geq N}) \to \forall m \in ℤ_{\geq N} X \in dom F (m)$
68		simpr	$⊢ (φ \land m \in ℤ_{\geq N}) \to m \in ℤ_{\geq N}$
69		rspa	$⊢ (\forall m \in ℤ_{\geq N} X \in dom F (m) \land m \in ℤ_{\geq N}) \to X \in dom F (m)$
70	67 68 69	syl2anc	$⊢ (φ \land m \in ℤ_{\geq N}) \to X \in dom F (m)$
71	63 70	ffvelrnd	$⊢ (φ \land m \in ℤ_{\geq N}) \to F (m) (X) \in ℝ$
72	54 56 71	syl2anc	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in ℤ_{\geq n}) \to F (m) (X) \in ℝ$
73		eluzelz	$⊢ n \in ℤ_{\geq N} \to n \in ℤ$
74	73	adantl	$⊢ (φ \land n \in ℤ_{\geq N}) \to n \in ℤ$
75	3	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to M \in ℤ$
76		fvex	$⊢ F (m) (X) \in V$
77	76	a1i	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in Z) \to F (m) (X) \in V$
78	52 74 75 53 4 72 77	limsupequzmpt	$⊢ (φ \land n \in ℤ_{\geq N}) \to lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (X))) = lim sup ((m \in Z ⟼ F (m) (X)))$
79	9	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to lim sup ((m \in Z ⟼ F (m) (X))) \in ℝ$
80	78 79	eqeltrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (X))) \in ℝ$
81	80	renepnfd	$⊢ (φ \land n \in ℤ_{\geq N}) \to lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (X))) \neq +∞$
82	52 53 72 81	limsupubuzmpt	$⊢ (φ \land n \in ℤ_{\geq N}) \to \exists y \in ℝ \forall m \in ℤ_{\geq n} F (m) (X) \leq y$
83		uzid2	$⊢ n \in ℤ_{\geq N} \to n \in ℤ_{\geq n}$
84	83	ne0d	$⊢ n \in ℤ_{\geq N} \to ℤ_{\geq n} \neq \emptyset$
85	84	adantl	$⊢ (φ \land n \in ℤ_{\geq N}) \to ℤ_{\geq n} \neq \emptyset$
86	52 85 72	supxrre3rnmpt	$⊢ (φ \land n \in ℤ_{\geq N}) \to (sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{*} <) \in ℝ \leftrightarrow \exists y \in ℝ \forall m \in ℤ_{\geq n} F (m) (X) \leq y)$
87	82 86	mpbird	$⊢ (φ \land n \in ℤ_{\geq N}) \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{*} <) \in ℝ$
88	44 50 87	elrabd	$⊢ (φ \land n \in ℤ_{\geq N}) \to X \in \{y \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{*} <) \in ℝ\}$
89		simpl	$⊢ (y = x \land m \in ℤ_{\geq n}) \to y = x$
90	89	fveq2d	$⊢ (y = x \land m \in ℤ_{\geq n}) \to F (m) (y) = F (m) (x)$
91	90	mpteq2dva	$⊢ y = x \to (m \in ℤ_{\geq n} ⟼ F (m) (y)) = (m \in ℤ_{\geq n} ⟼ F (m) (x))$
92	91	rneqd	$⊢ y = x \to ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) = ran (m \in ℤ_{\geq n} ⟼ F (m) (x))$
93	92	supeq1d	$⊢ y = x \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)$
94	93	eleq1d	$⊢ y = x \to (sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ)$
95	94	cbvrabv	$⊢ \{y \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\}$
96	88 95	eleqtrdi	$⊢ (φ \land n \in ℤ_{\geq N}) \to X \in \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
97		eqid	$⊢ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\}$
98		fvex	$⊢ F (m) \in V$
99	98	dmex	$⊢ dom F (m) \in V$
100	99	rgenw	$⊢ \forall m \in ℤ_{\geq n} dom F (m) \in V$
101	100	a1i	$⊢ n \in ℤ_{\geq N} \to \forall m \in ℤ_{\geq n} dom F (m) \in V$
102	84 101	iinexd	$⊢ n \in ℤ_{\geq N} \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
103	102	adantl	$⊢ (φ \land n \in ℤ_{\geq N}) \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
104	97 103	rabexd	$⊢ (φ \land n \in ℤ_{\geq N}) \to \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\} \in V$
105	7	fvmpt2	$⊢ (n \in Z \land \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} \in V) \to E (n) = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\}$
106	18 104 105	syl2anc	$⊢ (φ \land n \in ℤ_{\geq N}) \to E (n) = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
107	96 106	eleqtrrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to X \in E (n)$
108	38 43 107 87	fvmptd3	$⊢ (φ \land n \in ℤ_{\geq N}) \to (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) (X) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{} <)$
109	30 108	eqtrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to H (n) (X) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{*} <)$
110	1 109	mpteq2da	$⊢ φ \to (n \in ℤ_{\geq N} ⟼ H (n) (X)) = (n \in ℤ_{\geq N} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{*} <))$
111	4	eluzelz2	$⊢ N \in Z \to N \in ℤ$
112	10 111	syl	$⊢ φ \to N \in ℤ$
113		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
114	76	a1i	$⊢ (φ \land m \in ℤ_{\geq N}) \to F (m) (X) \in V$
115	76	a1i	$⊢ (φ \land m \in Z) \to F (m) (X) \in V$
116	2 112 3 113 4 114 115	limsupequzmpt	$⊢ φ \to lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X))) = lim sup ((m \in Z ⟼ F (m) (X)))$
117	116 9	eqeltrd	$⊢ φ \to lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X))) \in ℝ$
118	2 112 113 71 117	supcnvlimsupmpt	$⊢ φ \to (n \in ℤ_{\geq N} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{*} <)) ⇝ lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X)))$
119	110 118	eqbrtrd	$⊢ φ \to (n \in ℤ_{\geq N} ⟼ H (n) (X)) ⇝ lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X)))$

Metamath Proof Explorer

Theorem smflimsuplem5

Proof