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	biimpi	$⊢ 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	32	adantl	$⊢ (φ \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)\}$
34		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)\}$
35	3	adantr	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to S \in SAlg$
36	4	ffvelcdmda	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
37	36	adantrr	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to F (m) \in SMblFn (S)$
38		eqid	$⊢ dom F (m) = dom F (m)$
39	7	adantr	$⊢ (φ \land k \in ℕ) \to A \in ℝ$
40		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
41	40	adantl	$⊢ (φ \land k \in ℕ) \to \frac{1}{k} \in ℝ$
42	39 41	readdcld	$⊢ (φ \land k \in ℕ) \to A + (\frac{1}{k}) \in ℝ$
43	42	adantrl	$⊢ (φ \land (m \in Z \land k \in ℕ)) \to A + (\frac{1}{k}) \in ℝ$
44	35 37 38 43	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))$
45		fvex	$⊢ F (m) \in V$
46	45	dmex	$⊢ dom F (m) \in V$
47	46	a1i	$⊢ φ \to dom F (m) \in V$
48		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))$
49	3 47 48	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))$
50	49	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))$
51	44 50	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)$
52		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)$
53	51 52	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$
54	53	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$
55	34 54	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$
56	55	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))$
57	56	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)$
58	57	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)$
59	33 58	mpd	$⊢ (φ \land y \in ran P) \to y \neq \emptyset$
60	28 59	axccd2	$⊢ φ \to \exists c \forall y \in ran P c (y) \in y$
61	1	adantr	$⊢ (φ \land \forall y \in ran P c (y) \in y) \to M \in ℤ$
62	3	adantr	$⊢ (φ \land \forall y \in ran P c (y) \in y) \to S \in SAlg$
63	4	adantr	$⊢ (φ \land \forall y \in ran P c (y) \in y) \to F : Z ⟶ SMblFn (S)$
64	7	adantr	$⊢ (φ \land \forall y \in ran P c (y) \in y) \to A \in ℝ$
65		fvoveq1	$⊢ l = m \to c (l P j) = c (m P j)$
66		oveq2	$⊢ j = k \to m P j = m P k$
67	66	fveq2d	$⊢ j = k \to c (m P j) = c (m P k)$
68	65 67	cbvmpov	$⊢ (l \in Z, j \in ℕ ⟼ c (l P j)) = (m \in Z, k \in ℕ ⟼ c (m P k))$
69		nfcv	$⊢ \underline{Ⅎ} k ⋃_{n \in Z} ⋂_{i \in ℤ_{\geq n}} (i (l \in Z, j \in ℕ ⟼ c (l P j)) j)$
70		nfcv	$⊢ \underline{Ⅎ} j Z$
71		nfcv	$⊢ \underline{Ⅎ} j ℤ_{\geq n}$
72		nfcv	$⊢ \underline{Ⅎ} j m$
73		nfmpo2	$⊢ \underline{Ⅎ} j (l \in Z, j \in ℕ ⟼ c (l P j))$
74		nfcv	$⊢ \underline{Ⅎ} j k$
75	72 73 74	nfov	$⊢ \underline{Ⅎ} j (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
76	71 75	nfiin	$⊢ \underline{Ⅎ} j ⋂_{m \in ℤ_{\geq n}} (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
77	70 76	nfiun	$⊢ \underline{Ⅎ} j ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m (l \in Z, j \in ℕ ⟼ c (l P j)) k)$
78		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$
79	78	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$
80	79	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)$
81		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$
82	81	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)$
83	82	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)$
84	80 83	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)$
85	84	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)$
86	85	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)$
87	69 77 86	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)$
88		fveq2	$⊢ y = r \to c (y) = c (r)$
89		id	$⊢ y = r \to y = r$
90	88 89	eleq12d	$⊢ y = r \to (c (y) \in y \leftrightarrow c (r) \in r)$
91	90	rspccva	$⊢ (\forall y \in ran P c (y) \in y \land r \in ran P) \to c (r) \in r$
92	91	adantll	$⊢ ((φ \land \forall y \in ran P c (y) \in y) \land r \in ran P) \to c (r) \in r$
93	61 2 62 63 5 6 64 8 68 87 92	smflimlem5	$⊢ (φ \land \forall y \in ran P c (y) \in y) \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D)$
94	93	ex	$⊢ φ \to (\forall y \in ran P c (y) \in y \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D))$
95	94	exlimdv	$⊢ φ \to (\exists c \forall y \in ran P c (y) \in y \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D))$
96	60 95	mpd	$⊢ φ \to \{x \in D \| G (x) \leq A\} \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smflimlem6

Proof