# 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 ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
smff.f ${⊢}{\phi }\to {F}\in \mathrm{SMblFn}\left({S}\right)$
smff.d ${⊢}{D}=\mathrm{dom}{F}$
Assertion smff ${⊢}{\phi }\to {F}:{D}⟶ℝ$

### Proof

Step Hyp Ref Expression
1 smff.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
2 smff.f ${⊢}{\phi }\to {F}\in \mathrm{SMblFn}\left({S}\right)$
3 smff.d ${⊢}{D}=\mathrm{dom}{F}$
4 1 3 issmf ${⊢}{\phi }\to \left({F}\in \mathrm{SMblFn}\left({S}\right)↔\left({D}\subseteq \bigcup {S}\wedge {F}:{D}⟶ℝ\wedge \forall {a}\in ℝ\phantom{\rule{.4em}{0ex}}\left\{{x}\in {D}|{F}\left({x}\right)<{a}\right\}\in \left({S}{↾}_{𝑡}{D}\right)\right)\right)$
5 2 4 mpbid ${⊢}{\phi }\to \left({D}\subseteq \bigcup {S}\wedge {F}:{D}⟶ℝ\wedge \forall {a}\in ℝ\phantom{\rule{.4em}{0ex}}\left\{{x}\in {D}|{F}\left({x}\right)<{a}\right\}\in \left({S}{↾}_{𝑡}{D}\right)\right)$
6 5 simp2d ${⊢}{\phi }\to {F}:{D}⟶ℝ$