Metamath Proof Explorer

Theorem issmf

Description: The predicate " F is a real-valued measurable function w.r.t. to the sigma-algebra S ". 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 F is required to be a subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (i) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmf.s ⊢φ→S∈SAlg
issmf.d ⊢D=dom⁡F
Assertion issmf ⊢φ→F∈SMblFn⁡S↔D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝx∈D|F⁡x<a∈S↾𝑡D

Proof

Step Hyp Ref Expression
1 issmf.s ⊢φ→S∈SAlg
2 issmf.d ⊢D=dom⁡F
3 1 2 issmflem ⊢φ→F∈SMblFn⁡S↔D⊆⋃S∧F:D⟶ℝ∧∀b∈ℝy∈D|F⁡y<b∈S↾𝑡D
4 breq2 ⊢b=a→F⁡y<b↔F⁡y<a
5 4 rabbidv ⊢b=a→y∈D|F⁡y<b=y∈D|F⁡y<a
6 5 eleq1d ⊢b=a→y∈D|F⁡y<b∈S↾𝑡D↔y∈D|F⁡y<a∈S↾𝑡D
7 fveq2 ⊢y=x→F⁡y=F⁡x
8 7 breq1d ⊢y=x→F⁡y<a↔F⁡x<a
9 8 cbvrabv ⊢y∈D|F⁡y<a=x∈D|F⁡x<a
10 9 eleq1i ⊢y∈D|F⁡y<a∈S↾𝑡D↔x∈D|F⁡x<a∈S↾𝑡D
11 10 a1i ⊢b=a→y∈D|F⁡y<a∈S↾𝑡D↔x∈D|F⁡x<a∈S↾𝑡D
12 6 11 bitrd ⊢b=a→y∈D|F⁡y<b∈S↾𝑡D↔x∈D|F⁡x<a∈S↾𝑡D
13 12 cbvralvw ⊢∀b∈ℝy∈D|F⁡y<b∈S↾𝑡D↔∀a∈ℝx∈D|F⁡x<a∈S↾𝑡D
14 13 3anbi3i ⊢D⊆⋃S∧F:D⟶ℝ∧∀b∈ℝy∈D|F⁡y<b∈S↾𝑡D↔D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝx∈D|F⁡x<a∈S↾𝑡D
15 14 a1i ⊢φ→D⊆⋃S∧F:D⟶ℝ∧∀b∈ℝy∈D|F⁡y<b∈S↾𝑡D↔D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝx∈D|F⁡x<a∈S↾𝑡D
16 3 15 bitrd ⊢φ→F∈SMblFn⁡S↔D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝx∈D|F⁡x<a∈S↾𝑡D