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 . The proof uses fnrndomnum rather than fnrndomg , and so does not require ax-ac . (Contributed by Glauco Siliprandi, 26-Jun-2021) (Revised by Vincent Gonzalez, 30-Aug-2026)

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

Metamath Proof Explorer

Theorem smflimlem6

Proof