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