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 ⊢ Ⅎ _ x F
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 ⊢ Ⅎ _ x F
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 ⊢ Ⅎ _ y D
6 1 nfdm ⊢ Ⅎ _ x dom ⁡ F
7 3 6 nfcxfr ⊢ Ⅎ _ x D
8 nfcv ⊢ Ⅎ _ x y
9 1 8 nffv ⊢ Ⅎ _ x F ⁡ y
10 nfcv ⊢ Ⅎ _ x <
11 nfcv ⊢ Ⅎ _ x a
12 9 10 11 nfbr ⊢ Ⅎ x F ⁡ y < a
13 nfv ⊢ Ⅎ y F ⁡ 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