smflimsuplem1

Description: If H converges, the limsup of F is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smflimsuplem1.z	$⊢ Z = ℤ_{\geq M}$
	smflimsuplem1.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
	smflimsuplem1.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
	smflimsuplem1.k	$⊢ φ \to K \in Z$
Assertion	smflimsuplem1	$⊢ φ \to dom H (K) \subseteq dom F (K)$

Proof

Step	Hyp	Ref	Expression
1		smflimsuplem1.z	$⊢ Z = ℤ_{\geq M}$
2		smflimsuplem1.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
3		smflimsuplem1.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
4		smflimsuplem1.k	$⊢ φ \to K \in Z$
5		fveq2	$⊢ m = j \to F (m) = F (j)$
6	5	fveq1d	$⊢ m = j \to F (m) (x) = F (j) (x)$
7	6	cbvmptv	$⊢ (m \in ℤ_{\geq n} ⟼ F (m) (x)) = (j \in ℤ_{\geq n} ⟼ F (j) (x))$
8	7	rneqi	$⊢ ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) = ran (j \in ℤ_{\geq n} ⟼ F (j) (x))$
9	8	supeq1i	$⊢ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) = sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <)$
10	9	mpteq2i	$⊢ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) = (x \in E (n) ⟼ sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <))$
11	10	a1i	$⊢ n = K \to (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) = (x \in E (n) ⟼ sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <))$
12		fveq2	$⊢ n = K \to E (n) = E (K)$
13		fveq2	$⊢ n = K \to ℤ_{\geq n} = ℤ_{\geq K}$
14	13	mpteq1d	$⊢ n = K \to (j \in ℤ_{\geq n} ⟼ F (j) (x)) = (j \in ℤ_{\geq K} ⟼ F (j) (x))$
15	14	rneqd	$⊢ n = K \to ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) = ran (j \in ℤ_{\geq K} ⟼ F (j) (x))$
16	15	supeq1d	$⊢ n = K \to sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <) = sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <)$
17	12 16	mpteq12dv	$⊢ n = K \to (x \in E (n) ⟼ sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <)) = (x \in E (K) ⟼ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <))$
18	11 17	eqtrd	$⊢ n = K \to (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) = (x \in E (K) ⟼ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <))$
19		fvex	$⊢ E (K) \in V$
20	19	mptex	$⊢ (x \in E (K) ⟼ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <)) \in V$
21	20	a1i	$⊢ φ \to (x \in E (K) ⟼ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <)) \in V$
22	3 18 4 21	fvmptd3	$⊢ φ \to H (K) = (x \in E (K) ⟼ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <))$
23	22	dmeqd	$⊢ φ \to dom H (K) = dom (x \in E (K) ⟼ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <))$
24		xrltso	$⊢ < Or ℝ^{*}$
25	24	supex	$⊢ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <) \in V$
26		eqid	$⊢ (x \in E (K) ⟼ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <)) = (x \in E (K) ⟼ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <))$
27	25 26	dmmpti	$⊢ dom (x \in E (K) ⟼ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <)) = E (K)$
28	27	a1i	$⊢ φ \to dom (x \in E (K) ⟼ sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <)) = E (K)$
29	5	dmeqd	$⊢ m = j \to dom F (m) = dom F (j)$
30	29	cbviinv	$⊢ ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{j \in ℤ_{\geq n}} dom F (j)$
31	30	eleq2i	$⊢ x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow x \in ⋂_{j \in ℤ_{\geq n}} dom F (j)$
32	9	eleq1i	$⊢ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <) \in ℝ$
33	31 32	anbi12i	$⊢ (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ) \leftrightarrow (x \in ⋂_{j \in ℤ_{\geq n}} dom F (j) \land sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <) \in ℝ)$
34	33	rabbia2	$⊢ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{j \in ℤ_{\geq n}} dom F (j) \| sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <) \in ℝ\}$
35	34	a1i	$⊢ n = K \to \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{j \in ℤ_{\geq n}} dom F (j) \| sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <) \in ℝ\}$
36	13	iineq1d	$⊢ n = K \to ⋂_{j \in ℤ_{\geq n}} dom F (j) = ⋂_{j \in ℤ_{\geq K}} dom F (j)$
37	36	eleq2d	$⊢ n = K \to (x \in ⋂_{j \in ℤ_{\geq n}} dom F (j) \leftrightarrow x \in ⋂_{j \in ℤ_{\geq K}} dom F (j))$
38	16	eleq1d	$⊢ n = K \to (sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <) \in ℝ)$
39	37 38	anbi12d	$⊢ n = K \to ((x \in ⋂_{j \in ℤ_{\geq n}} dom F (j) \land sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <) \in ℝ) \leftrightarrow (x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \land sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <) \in ℝ))$
40	39	rabbidva2	$⊢ n = K \to \{x \in ⋂_{j \in ℤ_{\geq n}} dom F (j) \| sup (ran (j \in ℤ_{\geq n} ⟼ F (j) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \| sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <) \in ℝ\}$
41	35 40	eqtrd	$⊢ n = K \to \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \| sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <) \in ℝ\}$
42		eqid	$⊢ \{x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \| sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \| sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{} <) \in ℝ\}$
43	1 4	eluzelz2d	$⊢ φ \to K \in ℤ$
44		uzid	$⊢ K \in ℤ \to K \in ℤ_{\geq K}$
45		ne0i	$⊢ K \in ℤ_{\geq K} \to ℤ_{\geq K} \neq \emptyset$
46	43 44 45	3syl	$⊢ φ \to ℤ_{\geq K} \neq \emptyset$
47		fvex	$⊢ F (j) \in V$
48	47	dmex	$⊢ dom F (j) \in V$
49	48	rgenw	$⊢ \forall j \in ℤ_{\geq K} dom F (j) \in V$
50	49	a1i	$⊢ φ \to \forall j \in ℤ_{\geq K} dom F (j) \in V$
51	46 50	iinexd	$⊢ φ \to ⋂_{j \in ℤ_{\geq K}} dom F (j) \in V$
52	42 51	rabexd	$⊢ φ \to \{x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \| sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <) \in ℝ\} \in V$
53	2 41 4 52	fvmptd3	$⊢ φ \to E (K) = \{x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \| sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <) \in ℝ\}$
54	23 28 53	3eqtrd	$⊢ φ \to dom H (K) = \{x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \| sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <) \in ℝ\}$
55		ssrab2	$⊢ \{x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \| sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <) \in ℝ\} \subseteq ⋂_{j \in ℤ_{\geq K}} dom F (j)$
56	55	a1i	$⊢ φ \to \{x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \| sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <) \in ℝ\} \subseteq ⋂_{j \in ℤ_{\geq K}} dom F (j)$
57	43 44	syl	$⊢ φ \to K \in ℤ_{\geq K}$
58		fveq2	$⊢ j = K \to F (j) = F (K)$
59	58	dmeqd	$⊢ j = K \to dom F (j) = dom F (K)$
60		ssid	$⊢ dom F (K) \subseteq dom F (K)$
61	60	a1i	$⊢ φ \to dom F (K) \subseteq dom F (K)$
62	57 59 61	iinssd	$⊢ φ \to ⋂_{j \in ℤ_{\geq K}} dom F (j) \subseteq dom F (K)$
63	56 62	sstrd	$⊢ φ \to \{x \in ⋂_{j \in ℤ_{\geq K}} dom F (j) \| sup (ran (j \in ℤ_{\geq K} ⟼ F (j) (x)) ℝ^{*} <) \in ℝ\} \subseteq dom F (K)$
64	54 63	eqsstrd	$⊢ φ \to dom H (K) \subseteq dom F (K)$

Metamath Proof Explorer

Theorem smflimsuplem1

Proof