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 φSSAlg
smff.f φFSMblFnS
smff.d D=domF
Assertion smff φF:D

Proof

Step Hyp Ref Expression
1 smff.s φSSAlg
2 smff.f φFSMblFnS
3 smff.d D=domF
4 1 3 issmf φFSMblFnSDSF:DaxD|Fx<aS𝑡D
5 2 4 mpbid φDSF:DaxD|Fx<aS𝑡D
6 5 simp2d φF:D