P. 468 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46701-46800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	preimaioomnf 46701*	Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝐵})
Theorem	preimageiingt 46702*	A preimage of a left-closed, unbounded above interval, expressed as an indexed intersection of preimages of open, unbounded above intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} = ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵})
Theorem	preimaleiinlt 46703*	A preimage of a left-open, right-closed, unbounded below interval, expressed as an indexed intersection of preimages of open, unbound below intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} = ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ 𝐵 < (𝐶 + (1 / 𝑛))})
Theorem	pimgtmnff 46704	Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -∞, is the whole domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} = 𝐴)
Theorem	pimgtmnf 46705*	Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -∞, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} = 𝐴)
Theorem	pimrecltneg 46706	The preimage of an unbounded below, open interval, with negative upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 0)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)})
Theorem	salpreimagtge 46707*	If all the preimages of left-open, unbounded above intervals, belong to a sigma-algebra, then all the preimages of left-closed, unbounded above intervals, belong to the sigma-algebra. (iii) implies (iv) in Proposition 121B of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝑎 < 𝐵} ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} ∈ 𝑆)
Theorem	salpreimaltle 46708*	If all the preimages of right-open, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-closed, unbounded below intervals, belong to the sigma-algebra. (i) implies (ii) in Proposition 121B of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎} ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} ∈ 𝑆)
Theorem	issmflem 46709*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (i) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
Theorem	issmf 46710*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (i) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
Theorem	salpreimalelt 46711*	If all the preimages of right-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-open, unbounded below intervals, belong to the sigma-algebra. (ii) implies (i) in Proposition 121B of [Fremlin1] p. 36. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐴 = ∪ 𝑆    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎} ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} ∈ 𝑆)
Theorem	salpreimagtlt 46712*	If all the preimages of lef-open, unbounded above intervals, belong to a sigma-algebra, then all the preimages of right-open, unbounded below intervals, belong to the sigma-algebra. (iii) implies (i) in Proposition 121B of [Fremlin1] p. 36. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐴 = ∪ 𝑆    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝑎 < 𝐵} ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} ∈ 𝑆)
Theorem	smfpreimalt 46713*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	smff 46714	A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
Theorem	smfdmss 46715	The domain of a function measurable w.r.t. to a sigma-algebra, is a subset of the set underlying the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)
Theorem	issmff 46716*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (i) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
Theorem	issmfd 46717*	A sufficient condition for "𝐹 being a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	smfpreimaltf 46718*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	issmfdf 46719*	A sufficient condition for "𝐹 being a measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	sssmf 46720	The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ (SMblFn‘𝑆))
Theorem	mbfresmf 46721	A real-valued measurable function is a sigma-measurable function (w.r.t. the Lebesgue measure on the Reals). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)    &   ⊢ 𝑆 = dom vol    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	cnfsmf 46722	A continuous function is measurable. Proposition 121D (b) of [Fremlin1] p. 36 is a special case of this theorem, where the topology on the domain is induced by the standard topology on n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t dom 𝐹) Cn 𝐾))    &   ⊢ 𝑆 = (SalGen‘𝐽)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	incsmflem 46723*	A nondecreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝑅}    &   ⊢ 𝐶 = sup(𝑌, ℝ*, < )    &   ⊢ 𝐷 = (-∞(,)𝐶)    &   ⊢ 𝐸 = (-∞(,]𝐶)    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ 𝐵 𝑌 = (𝑏 ∩ 𝐴))
Theorem	incsmf 46724*	A real-valued, nondecreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐵))
Theorem	smfsssmf 46725	If a function is measurable w.r.t. to a sigma-algebra, then it is measurable w.r.t. to a larger sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑅 ∈ SAlg)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑅))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	issmflelem 46726*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all right-closed intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (ii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≤ 𝑎} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	issmfle 46727*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all right-closed intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be b subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (ii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≤ 𝑎} ∈ (𝑆 ↾t 𝐷))))
Theorem	smfpimltmpt 46728*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∈ (𝑆 ↾t 𝐴))
Theorem	smfpimltxr 46729*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	issmfdmpt 46730*	A sufficient condition for "𝐹 being a measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎} ∈ (𝑆 ↾t 𝐴))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))
Theorem	smfconst 46731*	Given a sigma-algebra over a base set X, every partial real-valued constant function is measurable. Proposition 121E (a) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	sssmfmpt 46732*	The restriction of a sigma-measurable function is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆))
Theorem	cnfrrnsmf 46733	A function, continuous from the standard topology on the space of n-dimensional reals to the standard topology on the reals, is Borel measurable. Proposition 121D (b) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝑋))    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t dom 𝐹) Cn 𝐾))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐵))
Theorem	smfid 46734*	The identity function is Borel sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑥) ∈ (SMblFn‘𝐵))
Theorem	bormflebmf 46735	A Borel measurable function is Lebesgue measurable. Proposition 121D (a) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ 𝐵 = (SalGen‘(TopOpen‘(ℝ^‘𝑋)))    &   ⊢ 𝐿 = dom (voln‘𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐵))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐿))
Theorem	smfpreimale 46736*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of a closed interval unbounded below is in the subspace sigma-algebra induced by its domain. See Proposition 121B (ii) of [Fremlin1] p. 35 (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	issmfgtlem 46737*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all left-open intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (iii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ (𝜑 → ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	issmfgt 46738*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all left-open intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be b subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (iii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))))
Theorem	issmfled 46739*	A sufficient condition for "𝐹 being a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≤ 𝑎} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	smfpimltxrmptf 46740*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∈ (𝑆 ↾t 𝐴))
Theorem	smfpimltxrmpt 46741*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∈ (𝑆 ↾t 𝐴))
Theorem	smfmbfcex 46742*	A constant function, with non-lebesgue-measurable domain is a sigma-measurable functions (w.r.t. the Lebesgue measure on the Reals) but it is not a measurable functions ( w.r.t. to df-mbf 25536). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑆 = dom vol    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ 0)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ∧ ¬ 𝐹 ∈ MblFn))
Theorem	issmfgtd 46743*	A sufficient condition for "𝐹 being a measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	smfpreimagt 46744*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ 𝐴 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))
Theorem	smfaddlem1 46745*	Given the sum of two functions, the preimage of an unbounded below, open interval, expressed as the countable union of intersections of preimages of both functions. Proposition 121E (b) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ 𝐾 = (𝑝 ∈ ℚ ↦ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})    ⇒   ⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
Theorem	smfaddlem2 46746*	The sum of two sigma-measurable functions is measurable. Proposition 121E (b) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐷) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ 𝐾 = (𝑝 ∈ ℚ ↦ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})    ⇒   ⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶)))
Theorem	smfadd 46747*	The sum of two sigma-measurable functions is measurable. Proposition 121E (b) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐷) ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ (𝐵 + 𝐷)) ∈ (SMblFn‘𝑆))
Theorem	decsmflem 46748*	A nonincreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)}    &   ⊢ 𝐶 = sup(𝑌, ℝ*, < )    &   ⊢ 𝐷 = (-∞(,)𝐶)    &   ⊢ 𝐸 = (-∞(,]𝐶)    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ 𝐵 𝑌 = (𝑏 ∩ 𝐴))
Theorem	decsmf 46749*	A real-valued, nonincreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐵))
Theorem	smfpreimagtf 46750*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ 𝐴 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))
Theorem	issmfgelem 46751*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all left-closed intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (iv) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ (𝜑 → ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	issmfge 46752*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all left-closed intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be b subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (iv) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))))
Theorem	smflimlem1 46753*	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 (𝐷 ∩ 𝐼) is in the subspace sigma-algebra induced by 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    &   ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))    &   ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟)    ⇒   ⊢ (𝜑 → (𝐷 ∩ 𝐼) ∈ (𝑆 ↾t 𝐷))
Theorem	smflimlem2 46754*	Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    &   ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))    &   ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ (𝐷 ∩ 𝐼))
Theorem	smflimlem3 46755*	The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    &   ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))    &   ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → (𝐶‘𝑦) ∈ 𝑦)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐷 ∩ 𝐼))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ+)    &   ⊢ (𝜑 → (1 / 𝐾) < 𝑌)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + 𝑌)))
Theorem	smflimlem4 46756*	Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    &   ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))    &   ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟)    ⇒   ⊢ (𝜑 → (𝐷 ∩ 𝐼) ⊆ {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴})
Theorem	smflimlem5 46757*	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 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    &   ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))    &   ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	smflimlem6 46758*	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 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	smflim 46759*	The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	nsssmfmbflem 46760*	The sigma-measurable functions (w.r.t. the Lebesgue measure on the Reals) are not a subset of the measurable functions. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑆 = dom vol    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ 0)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 ∈ (SMblFn‘𝑆) ∧ ¬ 𝑓 ∈ MblFn))
Theorem	nsssmfmbf 46761	The sigma-measurable functions (w.r.t. the Lebesgue measure on the Reals) are not a subset of the measurable functions. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑆 = dom vol    ⇒   ⊢ ¬ (SMblFn‘𝑆) ⊆ MblFn
Theorem	smfpimgtxr 46762*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ 𝐴 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))
Theorem	smfpimgtmpt 46763*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵} ∈ (𝑆 ↾t 𝐴))
Theorem	smfpreimage 46764*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of a closed interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ 𝐴 ≤ (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))
Theorem	mbfpsssmf 46765	Real-valued measurable functions are a proper subset of sigma-measurable functions (w.r.t. the Lebesgue measure on the reals). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑆 = dom vol    ⇒   ⊢ (MblFn ∩ (ℝ ↑pm ℝ)) ⊊ (SMblFn‘𝑆)
Theorem	smfpimgtxrmptf 46766*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵} ∈ (𝑆 ↾t 𝐴))
Theorem	smfpimgtxrmpt 46767*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵} ∈ (𝑆 ↾t 𝐴))
Theorem	smfpimioompt 46768*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} ∈ (𝑆 ↾t 𝐴))
Theorem	smfpimioo 46769	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (◡𝐹 “ (𝐴(,)𝐵)) ∈ (𝑆 ↾t 𝐷))
Theorem	smfresal 46770*	Given a sigma-measurable function, the subsets of ℝ whose preimage is in the sigma-algebra induced by the function's domain, form a sigma-algebra. First part of the proof of Proposition 121E (f) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ 𝑇 = {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}    ⇒   ⊢ (𝜑 → 𝑇 ∈ SAlg)
Theorem	smfrec 46771*	The reciprocal of a sigma-measurable functions is sigma-measurable. First part of Proposition 121E (e) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 0}    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (1 / 𝐵)) ∈ (SMblFn‘𝑆))
Theorem	smfres 46772	The restriction of sigma-measurable function is sigma-measurable. Proposition 121E (h) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ (SMblFn‘𝑆))
Theorem	smfmullem1 46773	The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝑉 ∈ ℝ)    &   ⊢ (𝜑 → (𝑈 · 𝑉) < 𝐴)    &   ⊢ 𝑋 = ((𝐴 − (𝑈 · 𝑉)) / (1 + ((abs‘𝑈) + (abs‘𝑉))))    &   ⊢ 𝑌 = if(1 ≤ 𝑋, 1, 𝑋)    &   ⊢ (𝜑 → 𝑃 ∈ ((𝑈 − 𝑌)(,)𝑈))    &   ⊢ (𝜑 → 𝑅 ∈ (𝑈(,)(𝑈 + 𝑌)))    &   ⊢ (𝜑 → 𝑆 ∈ ((𝑉 − 𝑌)(,)𝑉))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉(,)(𝑉 + 𝑌)))    &   ⊢ (𝜑 → 𝐻 ∈ (𝑃(,)𝑅))    &   ⊢ (𝜑 → 𝐼 ∈ (𝑆(,)𝑍))    ⇒   ⊢ (𝜑 → (𝐻 · 𝐼) < 𝐴)
Theorem	smfmullem2 46774*	The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝐾 = {𝑞 ∈ (ℚ ↑m (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝐴}    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝑉 ∈ ℝ)    &   ⊢ (𝜑 → (𝑈 · 𝑉) < 𝐴)    &   ⊢ (𝜑 → 𝑃 ∈ ℚ)    &   ⊢ (𝜑 → 𝑅 ∈ ℚ)    &   ⊢ (𝜑 → 𝑆 ∈ ℚ)    &   ⊢ (𝜑 → 𝑍 ∈ ℚ)    &   ⊢ (𝜑 → 𝑃 ∈ ((𝑈 − 𝑌)(,)𝑈))    &   ⊢ (𝜑 → 𝑅 ∈ (𝑈(,)(𝑈 + 𝑌)))    &   ⊢ (𝜑 → 𝑆 ∈ ((𝑉 − 𝑌)(,)𝑉))    &   ⊢ (𝜑 → 𝑍 ∈ (𝑉(,)(𝑉 + 𝑌)))    &   ⊢ 𝑋 = ((𝐴 − (𝑈 · 𝑉)) / (1 + ((abs‘𝑈) + (abs‘𝑉))))    &   ⊢ 𝑌 = if(1 ≤ 𝑋, 1, 𝑋)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐾 (𝑈 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝑉 ∈ ((𝑞‘2)(,)(𝑞‘3))))
Theorem	smfmullem3 46775*	The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ 𝐾 = {𝑞 ∈ (ℚ ↑m (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅}    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝑉 ∈ ℝ)    &   ⊢ (𝜑 → (𝑈 · 𝑉) < 𝑅)    &   ⊢ 𝑋 = ((𝑅 − (𝑈 · 𝑉)) / (1 + ((abs‘𝑈) + (abs‘𝑉))))    &   ⊢ 𝑌 = if(1 ≤ 𝑋, 1, 𝑋)    ⇒   ⊢ (𝜑 → ∃𝑞 ∈ 𝐾 (𝑈 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝑉 ∈ ((𝑞‘2)(,)(𝑞‘3))))
Theorem	smfmullem4 46776*	The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐷) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ 𝐾 = {𝑞 ∈ (ℚ ↑m (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅}    &   ⊢ 𝐸 = (𝑞 ∈ 𝐾 ↦ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})    ⇒   ⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶)))
Theorem	smfmul 46777*	The multiplication of two sigma-measurable functions is measurable. Proposition 121E (d) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐷) ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ (𝐵 · 𝐷)) ∈ (SMblFn‘𝑆))
Theorem	smfmulc1 46778*	A sigma-measurable function multiplied by a constant is sigma-measurable. Proposition 121E (c) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ (SMblFn‘𝑆))
Theorem	smfdiv 46779*	The fraction of two sigma-measurable functions is measurable. Proposition 121E (e) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐷) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐸 = {𝑥 ∈ 𝐶 ∣ 𝐷 ≠ 0}    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∩ 𝐸) ↦ (𝐵 / 𝐷)) ∈ (SMblFn‘𝑆))
Theorem	smfpimbor1lem1 46780*	Every open set belongs to 𝑇. This is the second step in the proof of Proposition 121E (f) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐺 ∈ 𝐽)    &   ⊢ 𝑇 = {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝑇)
Theorem	smfpimbor1lem2 46781*	Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐸)    &   ⊢ 𝑇 = {𝑒 ∈ 𝒫 ℝ ∣ (◡𝐹 “ 𝑒) ∈ (𝑆 ↾t 𝐷)}    ⇒   ⊢ (𝜑 → 𝑃 ∈ (𝑆 ↾t 𝐷))
Theorem	smfpimbor1 46782	Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐸)    ⇒   ⊢ (𝜑 → 𝑃 ∈ (𝑆 ↾t 𝐷))
Theorem	smf2id 46783*	Twice the identity function is Borel sigma-measurable (just an example, to test previous general theorems). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (2 · 𝑥)) ∈ (SMblFn‘𝐵))
Theorem	smfco 46784	The composition of a Borel sigma-measurable function with a sigma-measurable function, is sigma-measurable. Proposition 121E (g) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝐻 ∈ (SMblFn‘𝐵))    ⇒   ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ (SMblFn‘𝑆))
Theorem	smfneg 46785*	The negative of a sigma-measurable function is measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ (SMblFn‘𝑆))
Theorem	smffmptf 46786	A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ)
Theorem	smffmpt 46787*	A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ)
Theorem	smflim2 46788*	The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). TODO: this has fewer distinct variable conditions than smflim 46759 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfpimcclem 46789*	Lemma for smfpimcc 46790 given the choice function 𝐶. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝜑    &   ⊢ 𝑍 ∈ 𝑉    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑛) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑛))})) → (𝐶‘𝑦) ∈ 𝑦)    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝐶‘{𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑛) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑛))}))    ⇒   ⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))))
Theorem	smfpimcc 46790*	Given a countable set of sigma-measurable functions, and a Borel set 𝐴 there exists a choice function ℎ that, for each measurable function, chooses a measurable set that, when intersected with the function's domain, gives the preimage of 𝐴. This is a generalization of the observation at the beginning of the proof of Proposition 121F of [Fremlin1] p. 39 . The statement would also be provable for uncountable sets, but in most cases it will suffice to consider the countable case, and only the axiom of countable choice will be needed. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))))
Theorem	issmfle2d 46791*	A sufficient condition for "𝐹 being a measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (◡𝐹 “ (-∞(,]𝑎)) ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	smflimmpt 46792*	The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). 𝐴 can contain 𝑚 as a free variable, in other words it can be thought as an indexed collection 𝐴(𝑚). 𝐵 can be thought as a collection with two indices 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∣ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfsuplem1 46793*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐻:𝑍⟶𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (◡(𝐹‘𝑛) “ (-∞(,]𝐴)) = ((𝐻‘𝑛) ∩ dom (𝐹‘𝑛)))    ⇒   ⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷))
Theorem	smfsuplem2 46794*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (◡𝐺 “ (-∞(,]𝐴)) ∈ (𝑆 ↾t 𝐷))
Theorem	smfsuplem3 46795*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfsup 46796*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfsupmpt 46797*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 𝐴 ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfsupxr 46798*	The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ*, < ) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ*, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfinflem 46799*	The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfinf 46800*	The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑛𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))