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
|- ( ph -> S e. SAlg )
smff.f
|- ( ph -> F e. ( SMblFn ` S ) )
smff.d
|- D = dom F
Assertion smff
|- ( ph -> F : D --> RR )

Proof

Step Hyp Ref Expression
1 smff.s
 |-  ( ph -> S e. SAlg )
2 smff.f
 |-  ( ph -> F e. ( SMblFn ` S ) )
3 smff.d
 |-  D = dom F
4 1 3 issmf
 |-  ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) )
5 2 4 mpbid
 |-  ( ph -> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) )
6 5 simp2d
 |-  ( ph -> F : D --> RR )