smflimlem6

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	smflimlem6.1	$⊢ φ \to M \in ℤ$
	smflimlem6.2	$⊢ Z = ℤ_{\geq M}$
	smflimlem6.3	$⊢ φ \to S \in SAlg$
	smflimlem6.4	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflimlem6.5	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	smflimlem6.6	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
	smflimlem6.7	$⊢ φ \to A \in ℝ$
	smflimlem6.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)\})$
Assertion	smflimlem6	$⊢ φ \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D)$

Proof

Step	Hyp	Ref	Expression
1		smflimlem6.1	$⊢ φ \to M \in ℤ$
2		smflimlem6.2	$⊢ Z = ℤ_{\geq M}$
3		smflimlem6.3	$⊢ φ \to S \in SAlg$
4		smflimlem6.4	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smflimlem6.5	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
6		smflimlem6.6	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
7		smflimlem6.7	$⊢ φ \to A \in ℝ$
8		smflimlem6.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	2	fvexi	$⊢ Z \in V$
10		nnex	$⊢ ℕ \in V$
11	9 10	xpex	$⊢ Z \times ℕ \in V$
12	11	a1i	$⊢ φ \to Z \times ℕ \in V$
13		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)\}$
14	13 3	rabexd	$⊢ φ \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
15	14	adantr	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
16	15	ralrimivva	$⊢ φ \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$
17	8	fnmpo	$⊢ \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 P Fn (Z \times ℕ)$
18	16 17	syl	$⊢ φ \to P Fn (Z \times ℕ)$
19		fnrndomg	$⊢ Z \times ℕ \in V \to (P Fn (Z \times ℕ) \to ran P ≼ (Z \times ℕ))$
20	12 18 19	sylc	$⊢ φ \to ran P ≼ (Z \times ℕ)$
21	2	uzct	$⊢ Z ≼ ω$
22		nnct	$⊢ ℕ ≼ ω$
23	21 22	pm3.2i	$⊢ (Z ≼ ω \land ℕ ≼ ω)$
24		xpct	$⊢ (Z ≼ ω \land ℕ ≼ ω) \to (Z \times ℕ) ≼ ω$
25	23 24	ax-mp	$⊢ (Z \times ℕ) ≼ ω$
26	25	a1i	$⊢ φ \to (Z \times ℕ) ≼ ω$
27		domtr	$⊢ (ran P ≼ (Z \times ℕ) \land (Z \times ℕ) ≼ ω) \to ran P ≼ ω$
28	20 26 27	syl2anc	$⊢ φ \to ran P ≼ ω$
29		vex	$⊢ y \in V$
30	8	elrnmpog	$⊢ y \in V \to (y \in ran P \leftrightarrow \exists m \in Z \exists k \in ℕ y = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\})$
31	29 30	ax-mp	$⊢ y \in ran P \leftrightarrow \exists m \in Z \exists k \in ℕ y = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}$
32	31	bilani	$⊢ (φ \land y \in ran P) \to \exists m \in Z \exists k \in ℕ y = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}$
33		simp3	$⊢ (φ \land (m \in Z \land k \in ℕ) \land y = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}) \to y = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}$
34	3	adantr	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to S \in SAlg$
35	4	ffvelcdmda	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
36	35	adantrr	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to F (m) \in SMblFn (S)$
37		eqid	$⊢ dom F (m) = dom F (m)$
38	7	adantr	$⊢ (φ \land k \in ℕ) \to A \in ℝ$
39		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
40	39	adantl	$⊢ (φ \land k \in ℕ) \to \frac{1}{k} \in ℝ$
41	38 40	readdcld	$⊢ (φ \land k \in ℕ) \to A + (\frac{1}{k}) \in ℝ$
42	41	adantrl	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to A + (\frac{1}{k}) \in ℝ$
43	34 36 37 42	smfpreimalt	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \in (S ↾_{𝑡} dom F (m))$
44		fvex	$⊢ F (m) \in V$
45	44	dmex	$⊢ dom F (m) \in V$
46	45	a1i	$⊢ φ \to dom F (m) \in V$
47		elrest	$⊢ (S \in SAlg \land dom F (m) \in V) \to (\{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \in (S ↾_{𝑡} dom F (m)) \leftrightarrow \exists s \in S \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m))$
48	3 46 47	syl2anc	$⊢ φ \to (\{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \in (S ↾_{𝑡} dom F (m)) \leftrightarrow \exists s \in S \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m))$
49	48	adantr	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to (\{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \in (S ↾_{𝑡} dom F (m)) \leftrightarrow \exists s \in S \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m))$
50	43 49	mpbid	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to \exists s \in S \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)$
51		rabn0	$⊢ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \neq \emptyset \leftrightarrow \exists s \in S \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)$
52	50 51	sylibr	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \neq \emptyset$
53	52	3adant3	$⊢ (φ \land (m \in Z \land k \in ℕ) \land y = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}) \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \neq \emptyset$
54	33 53	eqnetrd	$⊢ (φ \land (m \in Z \land k \in ℕ) \land y = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}) \to y \neq \emptyset$
55	54	3exp	$⊢ φ \to ((m \in Z \land k \in ℕ) \to (y = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \to y \neq \emptyset))$
56	55	rexlimdvv	$⊢ φ \to (\exists m \in Z \exists k \in ℕ y = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \to y \neq \emptyset)$
57	56	adantr	$⊢ (φ \land y \in ran P) \to (\exists m \in Z \exists k \in ℕ y = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \to y \neq \emptyset)$
58	32 57	mpd	$⊢ (φ \land y \in ran P) \to y \neq \emptyset$
59	28 58	axccd2	$⊢ φ \to \exists c \forall y \in ran P c (y) \in y$
60	1	adantr	$⊢ (φ \land \forall y \in ran P c (y) \in y) \to M \in ℤ$
61	3	adantr	$⊢ (φ \land \forall y \in ran P c (y) \in y) \to S \in SAlg$
62	4	adantr	$⊢ (φ \land \forall y \in ran P c (y) \in y) \to F : Z ⟶ SMblFn (S)$
63	7	adantr	$⊢ (φ \land \forall y \in ran P c (y) \in y) \to A \in ℝ$
64		fvoveq1	$⊢ l = m \to c (l P j) = c (m P j)$
65		oveq2	$⊢ j = k \to m P j = m P k$
66	65	fveq2d	$⊢ j = k \to c (m P j) = c (m P k)$
67	64 66	cbvmpov	$⊢ (l \in Z, j \in ℕ ⟼ c (l P j)) = (m \in Z, k \in ℕ ⟼ c (m P k))$
68		nfcv	$⊢ \underline{Ⅎ} k ⋃_{n \in Z} ⋂_{i \in ℤ_{\geq n}} (i (l \in Z, j \in ℕ ⟼ c (l P j)) j)$
69		nfcv	$⊢ \underline{Ⅎ} j Z$
70		nfcv	$⊢ \underline{Ⅎ} j ℤ_{\geq n}$
71		nfcv	$⊢ \underline{Ⅎ} j m$
72		nfmpo2	$⊢ \underline{Ⅎ} j (l \in Z, j \in ℕ ⟼ c (l P j))$
73		nfcv	$⊢ \underline{Ⅎ} j k$
74	71 72 73	nfov	$⊢ \underline{Ⅎ} j (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
75	70 74	nfiin	$⊢ \underline{Ⅎ} j ⋂_{m \in ℤ_{\geq n}} (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
76	69 75	nfiun	$⊢ \underline{Ⅎ} j ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
77		oveq2	$⊢ j = k \to i (l \in Z, j \in ℕ ⟼ c (l P j)) j = i (l \in Z, j \in ℕ ⟼ c (l P j)) k$
78	77	adantr	$⊢ (j = k \land i \in ℤ_{\geq n}) \to i (l \in Z, j \in ℕ ⟼ c (l P j)) j = i (l \in Z, j \in ℕ ⟼ c (l P j)) k$
79	78	iineq2dv	$⊢ j = k \to ⋂_{i \in ℤ_{\geq n}} (i (l \in Z, j \in ℕ ⟼ c (l P j)) j) = ⋂_{i \in ℤ_{\geq n}} (i (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
80		oveq1	$⊢ i = m \to i (l \in Z, j \in ℕ ⟼ c (l P j)) k = m (l \in Z, j \in ℕ ⟼ c (l P j)) k$
81	80	cbviinv	$⊢ ⋂_{i \in ℤ_{\geq n}} (i (l \in Z, j \in ℕ ⟼ c (l P j)) k) = ⋂_{m \in ℤ_{\geq n}} (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
82	81	a1i	$⊢ j = k \to ⋂_{i \in ℤ_{\geq n}} (i (l \in Z, j \in ℕ ⟼ c (l P j)) k) = ⋂_{m \in ℤ_{\geq n}} (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
83	79 82	eqtrd	$⊢ j = k \to ⋂_{i \in ℤ_{\geq n}} (i (l \in Z, j \in ℕ ⟼ c (l P j)) j) = ⋂_{m \in ℤ_{\geq n}} (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
84	83	adantr	$⊢ (j = k \land n \in Z) \to ⋂_{i \in ℤ_{\geq n}} (i (l \in Z, j \in ℕ ⟼ c (l P j)) j) = ⋂_{m \in ℤ_{\geq n}} (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
85	84	iuneq2dv	$⊢ j = k \to ⋃_{n \in Z} ⋂_{i \in ℤ_{\geq n}} (i (l \in Z, j \in ℕ ⟼ c (l P j)) j) = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
86	68 76 85	cbviin	$⊢ ⋂_{j \in ℕ} ⋃_{n \in Z} ⋂_{i \in ℤ_{\geq n}} (i (l \in Z, j \in ℕ ⟼ c (l P j)) j) = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
87		fveq2	$⊢ y = r \to c (y) = c (r)$
88		id	$⊢ y = r \to y = r$
89	87 88	eleq12d	$⊢ y = r \to (c (y) \in y \leftrightarrow c (r) \in r)$
90	89	rspccva	$⊢ (\forall y \in ran P c (y) \in y \land r \in ran P) \to c (r) \in r$
91	90	adantll	$⊢ ((φ \land \forall y \in ran P c (y) \in y) \land r \in ran P) \to c (r) \in r$
92	60 2 61 62 5 6 63 8 67 86 91	smflimlem5	$⊢ (φ \land \forall y \in ran P c (y) \in y) \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D)$
93	92	ex	$⊢ φ \to (\forall y \in ran P c (y) \in y \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D))$
94	93	exlimdv	$⊢ φ \to (\exists c \forall y \in ran P c (y) \in y \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D))$
95	59 94	mpd	$⊢ φ \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smflimlem6

Proof