smflimlem5

Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smflimlem5.1	$⊢ φ \to M \in ℤ$
	smflimlem5.2	$⊢ Z = ℤ_{\geq M}$
	smflimlem5.3	$⊢ φ \to S \in SAlg$
	smflimlem5.4	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflimlem5.5	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	smflimlem5.6	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
	smflimlem5.7	$⊢ φ \to A \in ℝ$
	smflimlem5.8	$⊢ 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)\})$
	smflimlem5.9	$⊢ H = (m \in Z, k \in ℕ ⟼ C (m P k))$
	smflimlem5.10	$⊢ I = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
	smflimlem5.11	$⊢ (φ \land r \in ran P) \to C (r) \in r$
Assertion	smflimlem5	$⊢ φ \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D)$

Proof

Step	Hyp	Ref	Expression
1		smflimlem5.1	$⊢ φ \to M \in ℤ$
2		smflimlem5.2	$⊢ Z = ℤ_{\geq M}$
3		smflimlem5.3	$⊢ φ \to S \in SAlg$
4		smflimlem5.4	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smflimlem5.5	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
6		smflimlem5.6	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
7		smflimlem5.7	$⊢ φ \to A \in ℝ$
8		smflimlem5.8	$⊢ 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)\})$
9		smflimlem5.9	$⊢ H = (m \in Z, k \in ℕ ⟼ C (m P k))$
10		smflimlem5.10	$⊢ I = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
11		smflimlem5.11	$⊢ (φ \land r \in ran P) \to C (r) \in r$
12	2 3 4 5 6 7 8 9 10 11	smflimlem2	$⊢ φ \to \{x \in D \| G (x) \leq A\} \subseteq D \cap I$
13	1 2 3 4 5 6 7 8 9 10 11	smflimlem4	$⊢ φ \to D \cap I \subseteq \{x \in D \| G (x) \leq A\}$
14	12 13	eqssd	$⊢ φ \to \{x \in D \| G (x) \leq A\} = D \cap I$
15	2 3 5 8 9 10 11	smflimlem1	$⊢ φ \to D \cap I \in (S ↾_{𝑡} D)$
16	14 15	eqeltrd	$⊢ φ \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smflimlem5

Proof