smflimlem1

Description: Lemma for the proof that the limit of a sequence of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves that ( D i^i I ) is in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smflimlem1.1	$⊢ Z = ℤ_{\geq M}$
	smflimlem1.2	$⊢ φ \to S \in SAlg$
	smflimlem1.3	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	smflimlem1.4	$⊢ P = (m \in Z, k \in ℕ ⟼ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\})$
	smflimlem1.5	$⊢ H = (m \in Z, k \in ℕ ⟼ C (m P k))$
	smflimlem1.6	$⊢ I = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
	smflimlem1.7	$⊢ (φ \land r \in ran P) \to C (r) \in r$
Assertion	smflimlem1	$⊢ φ \to D \cap I \in (S ↾_{𝑡} D)$

Proof

Step	Hyp	Ref	Expression
1		smflimlem1.1	$⊢ Z = ℤ_{\geq M}$
2		smflimlem1.2	$⊢ φ \to S \in SAlg$
3		smflimlem1.3	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
4		smflimlem1.4	$⊢ P = (m \in Z, k \in ℕ ⟼ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\})$
5		smflimlem1.5	$⊢ H = (m \in Z, k \in ℕ ⟼ C (m P k))$
6		smflimlem1.6	$⊢ I = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
7		smflimlem1.7	$⊢ (φ \land r \in ran P) \to C (r) \in r$
8		fvex	$⊢ ℤ_{\geq M} \in V$
9	1 8	eqeltri	$⊢ Z \in V$
10		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
11	1	eleq2i	$⊢ n \in Z \leftrightarrow n \in ℤ_{\geq M}$
12	11	biimpi	$⊢ n \in Z \to n \in ℤ_{\geq M}$
13	10 12	sselid	$⊢ n \in Z \to n \in ℤ$
14		uzid	$⊢ n \in ℤ \to n \in ℤ_{\geq n}$
15	13 14	syl	$⊢ n \in Z \to n \in ℤ_{\geq n}$
16	15	ne0d	$⊢ n \in Z \to ℤ_{\geq n} \neq \emptyset$
17		fvex	$⊢ F (m) \in V$
18	17	dmex	$⊢ dom F (m) \in V$
19	18	rgenw	$⊢ \forall m \in ℤ_{\geq n} dom F (m) \in V$
20	19	a1i	$⊢ n \in Z \to \forall m \in ℤ_{\geq n} dom F (m) \in V$
21		iinexg	$⊢ (ℤ_{\geq n} \neq \emptyset \land \forall m \in ℤ_{\geq n} dom F (m) \in V) \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
22	16 20 21	syl2anc	$⊢ n \in Z \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
23	22	rgen	$⊢ \forall n \in Z ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
24		iunexg	$⊢ (Z \in V \land \forall n \in Z ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V) \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
25	9 23 24	mp2an	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
26	25	rabex	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} \in V$
27	3 26	eqeltri	$⊢ D \in V$
28	27	a1i	$⊢ φ \to D \in V$
29		nnct	$⊢ ℕ ≼ ω$
30	29	a1i	$⊢ φ \to ℕ ≼ ω$
31		nnn0	$⊢ ℕ \neq \emptyset$
32	31	a1i	$⊢ φ \to ℕ \neq \emptyset$
33	2	adantr	$⊢ (φ \land k \in ℕ) \to S \in SAlg$
34	1	uzct	$⊢ Z ≼ ω$
35	34	a1i	$⊢ (φ \land k \in ℕ) \to Z ≼ ω$
36	33	adantr	$⊢ ((φ \land k \in ℕ) \land n \in Z) \to S \in SAlg$
37		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
38	37	uzct	$⊢ ℤ_{\geq n} ≼ ω$
39	38	a1i	$⊢ ((φ \land k \in ℕ) \land n \in Z) \to ℤ_{\geq n} ≼ ω$
40	16	adantl	$⊢ ((φ \land k \in ℕ) \land n \in Z) \to ℤ_{\geq n} \neq \emptyset$
41		simpll	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to φ$
42	41	adantllr	$⊢ (((φ \land k \in ℕ) \land n \in Z) \land m \in ℤ_{\geq n}) \to φ$
43		simpll	$⊢ ((k \in ℕ \land n \in Z) \land m \in ℤ_{\geq n}) \to k \in ℕ$
44	43	adantlll	$⊢ (((φ \land k \in ℕ) \land n \in Z) \land m \in ℤ_{\geq n}) \to k \in ℕ$
45	1	uztrn2	$⊢ (n \in Z \land j \in ℤ_{\geq n}) \to j \in Z$
46	45	ssd	$⊢ n \in Z \to ℤ_{\geq n} \subseteq Z$
47	46	sselda	$⊢ (n \in Z \land m \in ℤ_{\geq n}) \to m \in Z$
48	47	adantll	$⊢ (((φ \land k \in ℕ) \land n \in Z) \land m \in ℤ_{\geq n}) \to m \in Z$
49		simp3	$⊢ (φ \land k \in ℕ \land m \in Z) \to m \in Z$
50		simp2	$⊢ (φ \land k \in ℕ \land m \in Z) \to k \in ℕ$
51		fvex	$⊢ C (m P k) \in V$
52	51	a1i	$⊢ (φ \land k \in ℕ \land m \in Z) \to C (m P k) \in V$
53	5	ovmpt4g	$⊢ (m \in Z \land k \in ℕ \land C (m P k) \in V) \to m H k = C (m P k)$
54	49 50 52 53	syl3anc	$⊢ (φ \land k \in ℕ \land m \in Z) \to m H k = C (m P k)$
55		simp1	$⊢ (φ \land k \in ℕ \land m \in Z) \to φ$
56		eqid	$⊢ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}$
57	56 2	rabexd	$⊢ φ \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
58	55 57	syl	$⊢ (φ \land k \in ℕ \land m \in Z) \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
59	4	ovmpt4g	$⊢ (m \in Z \land k \in ℕ \land \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V) \to m P k = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}$
60	49 50 58 59	syl3anc	$⊢ (φ \land k \in ℕ \land m \in Z) \to m P k = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}$
61		ssrab2	$⊢ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \subseteq S$
62	60 61	eqsstrdi	$⊢ (φ \land k \in ℕ \land m \in Z) \to m P k \subseteq S$
63	57	ralrimivw	$⊢ φ \to \forall k \in ℕ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
64	63	ralrimivw	$⊢ φ \to \forall m \in Z \forall k \in ℕ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
65	64	3ad2ant1	$⊢ (φ \land k \in ℕ \land m \in Z) \to \forall m \in Z \forall k \in ℕ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
66	4	elrnmpoid	$⊢ (m \in Z \land k \in ℕ \land \forall m \in Z \forall k \in ℕ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V) \to m P k \in ran P$
67	49 50 65 66	syl3anc	$⊢ (φ \land k \in ℕ \land m \in Z) \to m P k \in ran P$
68		ovex	$⊢ m P k \in V$
69		eleq1	$⊢ r = m P k \to (r \in ran P \leftrightarrow m P k \in ran P)$
70	69	anbi2d	$⊢ r = m P k \to ((φ \land r \in ran P) \leftrightarrow (φ \land m P k \in ran P))$
71		fveq2	$⊢ r = m P k \to C (r) = C (m P k)$
72		id	$⊢ r = m P k \to r = m P k$
73	71 72	eleq12d	$⊢ r = m P k \to (C (r) \in r \leftrightarrow C (m P k) \in (m P k))$
74	70 73	imbi12d	$⊢ r = m P k \to (((φ \land r \in ran P) \to C (r) \in r) \leftrightarrow ((φ \land m P k \in ran P) \to C (m P k) \in (m P k)))$
75	68 74 7	vtocl	$⊢ (φ \land m P k \in ran P) \to C (m P k) \in (m P k)$
76	55 67 75	syl2anc	$⊢ (φ \land k \in ℕ \land m \in Z) \to C (m P k) \in (m P k)$
77	62 76	sseldd	$⊢ (φ \land k \in ℕ \land m \in Z) \to C (m P k) \in S$
78	54 77	eqeltrd	$⊢ (φ \land k \in ℕ \land m \in Z) \to m H k \in S$
79	42 44 48 78	syl3anc	$⊢ (((φ \land k \in ℕ) \land n \in Z) \land m \in ℤ_{\geq n}) \to m H k \in S$
80	36 39 40 79	saliincl	$⊢ ((φ \land k \in ℕ) \land n \in Z) \to ⋂_{m \in ℤ_{\geq n}} (m H k) \in S$
81	33 35 80	saliuncl	$⊢ (φ \land k \in ℕ) \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) \in S$
82	2 30 32 81	saliincl	$⊢ φ \to ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) \in S$
83	6 82	eqeltrid	$⊢ φ \to I \in S$
84		incom	$⊢ D \cap I = I \cap D$
85	2 28 83 84	elrestd	$⊢ φ \to D \cap I \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smflimlem1

Proof