Metamath Proof Explorer

Theorem issmff

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 issmff.x ⊢Ⅎ_xF
issmff.s ⊢φ→S∈SAlg
issmff.d ⊢D=dom⁡F
Assertion issmff ⊢φ→F∈SMblFn⁡S↔D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝx∈D|F⁡x<a∈S↾𝑡D

Proof

Step Hyp Ref Expression
1 issmff.x ⊢Ⅎ_xF
2 issmff.s ⊢φ→S∈SAlg
3 issmff.d ⊢D=dom⁡F
4 2 3 issmf ⊢φ→F∈SMblFn⁡S↔D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝy∈D|F⁡y<a∈S↾𝑡D
5 nfcv ⊢Ⅎ_yD
6 1 nfdm ⊢Ⅎ_xdom⁡F
7 3 6 nfcxfr ⊢Ⅎ_xD
8 nfcv ⊢Ⅎ_xy
9 1 8 nffv ⊢Ⅎ_xF⁡y
10 nfcv ⊢Ⅎ_x<
11 nfcv ⊢Ⅎ_xa
12 9 10 11 nfbr ⊢ℲxF⁡y<a
13 nfv ⊢ℲyF⁡x<a
14 fveq2 ⊢y=x→F⁡y=F⁡x
15 14 breq1d ⊢y=x→F⁡y<a↔F⁡x<a
16 5 7 12 13 15 cbvrabw ⊢y∈D|F⁡y<a=x∈D|F⁡x<a
17 16 eleq1i ⊢y∈D|F⁡y<a∈S↾𝑡D↔x∈D|F⁡x<a∈S↾𝑡D
18 17 ralbii ⊢∀a∈ℝy∈D|F⁡y<a∈S↾𝑡D↔∀a∈ℝx∈D|F⁡x<a∈S↾𝑡D
19 18 3anbi3i ⊢D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝy∈D|F⁡y<a∈S↾𝑡D↔D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝx∈D|F⁡x<a∈S↾𝑡D
20 19 a1i ⊢φ→D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝy∈D|F⁡y<a∈S↾𝑡D↔D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝx∈D|F⁡x<a∈S↾𝑡D
21 4 20 bitrd ⊢φ→F∈SMblFn⁡S↔D⊆⋃S∧F:D⟶ℝ∧∀a∈ℝx∈D|F⁡x<a∈S↾𝑡D