Description: The domain of a measurable function is a subset of the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mbfdmssre | |- ( F e. MblFn -> dom F C_ RR ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ismbf1 | |- ( F e. MblFn <-> ( F e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) ) |
|
| 2 | 1 | simplbi | |- ( F e. MblFn -> F e. ( CC ^pm RR ) ) |
| 3 | elpmi2 | |- ( F e. ( CC ^pm RR ) -> dom F C_ RR ) |
|
| 4 | 2 3 | syl | |- ( F e. MblFn -> dom F C_ RR ) |