Metamath Proof Explorer


Theorem smff

Description: A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smff.s ( 𝜑𝑆 ∈ SAlg )
smff.f ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
smff.d 𝐷 = dom 𝐹
Assertion smff ( 𝜑𝐹 : 𝐷 ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 smff.s ( 𝜑𝑆 ∈ SAlg )
2 smff.f ( 𝜑𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3 smff.d 𝐷 = dom 𝐹
4 1 3 issmf ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝑆t 𝐷 ) ) ) )
5 2 4 mpbid ( 𝜑 → ( 𝐷 𝑆𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥𝐷 ∣ ( 𝐹𝑥 ) < 𝑎 } ∈ ( 𝑆t 𝐷 ) ) )
6 5 simp2d ( 𝜑𝐹 : 𝐷 ⟶ ℝ )