Description: A function, continuous from the standard topology on the space of n-dimensional reals to the standard topology on the reals, is Borel measurable. Proposition 121D (b) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cnfrrnsmf.x | |- ( ph -> X e. Fin ) |
|
| cnfrrnsmf.j | |- J = ( TopOpen ` ( RR^ ` X ) ) |
||
| cnfrrnsmf.k | |- K = ( topGen ` ran (,) ) |
||
| cnfrrnsmf.f | |- ( ph -> F e. ( ( J |`t dom F ) Cn K ) ) |
||
| cnfrrnsmf.b | |- B = ( SalGen ` J ) |
||
| Assertion | cnfrrnsmf | |- ( ph -> F e. ( SMblFn ` B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnfrrnsmf.x | |- ( ph -> X e. Fin ) |
|
| 2 | cnfrrnsmf.j | |- J = ( TopOpen ` ( RR^ ` X ) ) |
|
| 3 | cnfrrnsmf.k | |- K = ( topGen ` ran (,) ) |
|
| 4 | cnfrrnsmf.f | |- ( ph -> F e. ( ( J |`t dom F ) Cn K ) ) |
|
| 5 | cnfrrnsmf.b | |- B = ( SalGen ` J ) |
|
| 6 | 2 | rrxtop | |- ( X e. Fin -> J e. Top ) |
| 7 | 1 6 | syl | |- ( ph -> J e. Top ) |
| 8 | 7 3 4 5 | cnfsmf | |- ( ph -> F e. ( SMblFn ` B ) ) |