smflimsuplem3

Description: The limit of the ( Hn ) functions is sigma-measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		smflimsuplem3.m	$⊢ φ \to M \in ℤ$
2		smflimsuplem3.z	$⊢ Z = ℤ_{\geq M}$
3		smflimsuplem3.s	$⊢ φ \to S \in SAlg$
4		smflimsuplem3.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smflimsuplem3.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
6		smflimsuplem3.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
7		nfv	$⊢ Ⅎ n φ$
8		nfv	$⊢ Ⅎ x φ$
9		nfv	$⊢ Ⅎ k φ$
10		fvex	$⊢ H (n) \in V$
11	10	dmex	$⊢ dom H (n) \in V$
12	11	a1i	$⊢ (φ \land n \in Z) \to dom H (n) \in V$
13		fvexd	$⊢ (φ \land n \in Z \land x \in dom H (n)) \to H (n) (x) \in V$
14	3	adantr	$⊢ (φ \land n \in Z) \to S \in SAlg$
15	5	a1i	$⊢ φ \to E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
16		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 ℝ\}$
17	2	eluzelz2	$⊢ n \in Z \to n \in ℤ$
18		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
19	17 18	uzn0d	$⊢ n \in Z \to ℤ_{\geq n} \neq \emptyset$
20		fvex	$⊢ F (m) \in V$
21	20	dmex	$⊢ dom F (m) \in V$
22	21	rgenw	$⊢ \forall m \in ℤ_{\geq n} dom F (m) \in V$
23	22	a1i	$⊢ n \in Z \to \forall m \in ℤ_{\geq n} dom F (m) \in V$
24	19 23	iinexd	$⊢ n \in Z \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
25	24	adantl	$⊢ (φ \land n \in Z) \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
26	16 25	rabexd	$⊢ (φ \land n \in Z) \to \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\} \in V$
27	15 26	fvmpt2d	$⊢ (φ \land n \in Z) \to E (n) = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
28		fvres	$⊢ m \in ℤ_{\geq n} \to ({F ↾}_{ℤ_{\geq n}}) (m) = F (m)$
29	28	eqcomd	$⊢ m \in ℤ_{\geq n} \to F (m) = ({F ↾}_{ℤ_{\geq n}}) (m)$
30	29	adantl	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to F (m) = ({F ↾}_{ℤ_{\geq n}}) (m)$
31	30	dmeqd	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to dom F (m) = dom ({F ↾}_{ℤ_{\geq n}}) (m)$
32	31	iineq2dv	$⊢ (φ \land n \in Z) \to ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{m \in ℤ_{\geq n}} dom ({F ↾}_{ℤ_{\geq n}}) (m)$
33	32	eleq2d	$⊢ (φ \land n \in Z) \to (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow x \in ⋂_{m \in ℤ_{\geq n}} dom ({F ↾}_{ℤ_{\geq n}}) (m))$
34	29	fveq1d	$⊢ m \in ℤ_{\geq n} \to F (m) (x) = ({F ↾}_{ℤ_{\geq n}}) (m) (x)$
35	34	mpteq2ia	$⊢ (m \in ℤ_{\geq n} ⟼ F (m) (x)) = (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x))$
36	35	rneqi	$⊢ ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) = ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x))$
37	36	supeq1i	$⊢ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <)$
38	37	a1i	$⊢ (φ \land n \in Z) \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <)$
39	38	eleq1d	$⊢ (φ \land n \in Z) \to (sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <) \in ℝ)$
40	33 39	anbi12d	$⊢ (φ \land n \in Z) \to ((x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ) \leftrightarrow (x \in ⋂_{m \in ℤ_{\geq n}} dom ({F ↾}_{ℤ_{\geq n}}) (m) \land sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <) \in ℝ))$
41	40	rabbidva2	$⊢ (φ \land n \in Z) \to \{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 ↾}_{ℤ_{\geq n}}) (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <) \in ℝ\}$
42	27 41	eqtrd	$⊢ (φ \land n \in Z) \to E (n) = \{x \in ⋂_{m \in ℤ_{\geq n}} dom ({F ↾}_{ℤ_{\geq n}}) (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{*} <) \in ℝ\}$
43	42 38	mpteq12dv	$⊢ (φ \land n \in Z) \to (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) = (x \in \{x \in ⋂_{m \in ℤ_{\geq n}} dom ({F ↾}_{ℤ_{\geq n}}) (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <) \in ℝ\} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{*} <))$
44		nfcv	$⊢ \underline{Ⅎ} m ({F ↾}_{ℤ_{\geq n}})$
45		nfcv	$⊢ \underline{Ⅎ} x ({F ↾}_{ℤ_{\geq n}})$
46	17	adantl	$⊢ (φ \land n \in Z) \to n \in ℤ$
47	4	adantr	$⊢ (φ \land n \in Z) \to F : Z ⟶ SMblFn (S)$
48	2	eleq2i	$⊢ n \in Z \leftrightarrow n \in ℤ_{\geq M}$
49	48	biimpi	$⊢ n \in Z \to n \in ℤ_{\geq M}$
50		uzss	$⊢ n \in ℤ_{\geq M} \to ℤ_{\geq n} \subseteq ℤ_{\geq M}$
51	49 50	syl	$⊢ n \in Z \to ℤ_{\geq n} \subseteq ℤ_{\geq M}$
52	51 2	sseqtrrdi	$⊢ n \in Z \to ℤ_{\geq n} \subseteq Z$
53	52	adantl	$⊢ (φ \land n \in Z) \to ℤ_{\geq n} \subseteq Z$
54	47 53	fssresd	$⊢ (φ \land n \in Z) \to ({F ↾}_{ℤ_{\geq n}}) : ℤ_{\geq n} ⟶ SMblFn (S)$
55		eqid	$⊢ \{x \in ⋂_{m \in ℤ_{\geq n}} dom ({F ↾}_{ℤ_{\geq n}}) (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{m \in ℤ_{\geq n}} dom ({F ↾}_{ℤ_{\geq n}}) (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <) \in ℝ\}$
56		eqid	$⊢ (x \in \{x \in ⋂_{m \in ℤ_{\geq n}} dom ({F ↾}_{ℤ_{\geq n}}) (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <) \in ℝ\} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <)) = (x \in \{x \in ⋂_{m \in ℤ_{\geq n}} dom ({F ↾}_{ℤ_{\geq n}}) (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <) \in ℝ\} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <))$
57	44 45 46 18 14 54 55 56	smfsupxr	$⊢ (φ \land n \in Z) \to (x \in \{x \in ⋂_{m \in ℤ_{\geq n}} dom ({F ↾}_{ℤ_{\geq n}}) (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <) \in ℝ\} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ ({F ↾}_{ℤ_{\geq n}}) (m) (x)) ℝ^{} <)) \in SMblFn (S)$
58	43 57	eqeltrd	$⊢ (φ \land n \in Z) \to (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) \in SMblFn (S)$
59	58 6	fmptd	$⊢ φ \to H : Z ⟶ SMblFn (S)$
60	59	ffvelcdmda	$⊢ (φ \land n \in Z) \to H (n) \in SMblFn (S)$
61		eqid	$⊢ dom H (n) = dom H (n)$
62	14 60 61	smff	$⊢ (φ \land n \in Z) \to H (n) : dom H (n) ⟶ ℝ$
63	62	feqmptd	$⊢ (φ \land n \in Z) \to H (n) = (x \in dom H (n) ⟼ H (n) (x))$
64	63	eqcomd	$⊢ (φ \land n \in Z) \to (x \in dom H (n) ⟼ H (n) (x)) = H (n)$
65	64 60	eqeltrd	$⊢ (φ \land n \in Z) \to (x \in dom H (n) ⟼ H (n) (x)) \in SMblFn (S)$
66		eqid	$⊢ \{x \in ⋃_{k \in Z} ⋂_{n \in ℤ_{\geq k}} dom H (n) \| (n \in Z ⟼ H (n) (x)) \in dom ⇝\} = \{x \in ⋃_{k \in Z} ⋂_{n \in ℤ_{\geq k}} dom H (n) \| (n \in Z ⟼ H (n) (x)) \in dom ⇝\}$
67		eqid	$⊢ (x \in \{x \in ⋃_{k \in Z} ⋂_{n \in ℤ_{\geq k}} dom H (n) \| (n \in Z ⟼ H (n) (x)) \in dom ⇝\} ⟼ ⇝ ((n \in Z ⟼ H (n) (x)))) = (x \in \{x \in ⋃_{k \in Z} ⋂_{n \in ℤ_{\geq k}} dom H (n) \| (n \in Z ⟼ H (n) (x)) \in dom ⇝\} ⟼ ⇝ ((n \in Z ⟼ H (n) (x))))$
68	7 8 9 1 2 12 13 3 65 66 67	smflimmpt	$⊢ φ \to (x \in \{x \in ⋃_{k \in Z} ⋂_{n \in ℤ_{\geq k}} dom H (n) \| (n \in Z ⟼ H (n) (x)) \in dom ⇝\} ⟼ ⇝ ((n \in Z ⟼ H (n) (x)))) \in SMblFn (S)$

Metamath Proof Explorer

Theorem smflimsuplem3

Proof