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 ) |
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 ) |