Theorem cnfrrnsmf

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	$$⊢\phi \to X\in \mathrm{Fin}$$
	cnfrrnsmf.j
	cnfrrnsmf.k	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	cnfrrnsmf.f	$$⊢\phi \to F\in \left(\left(J{\upharpoonright }_{𝑡}\mathrm{dom}F\right)\mathrm{Cn}K\right)$$
	cnfrrnsmf.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
Assertion	cnfrrnsmf	$$⊢\phi \to F\in \mathrm{SMblFn}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnfrrnsmf.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		cnfrrnsmf.j
3		cnfrrnsmf.k	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
4		cnfrrnsmf.f	$$⊢\phi \to F\in \left(\left(J{\upharpoonright }_{𝑡}\mathrm{dom}F\right)\mathrm{Cn}K\right)$$
5		cnfrrnsmf.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
6	2	rrxtop	$$⊢X\in \mathrm{Fin}\to J\in \mathrm{Top}$$
7	1 6	syl	$$⊢\phi \to J\in \mathrm{Top}$$
8	7 3 4 5	cnfsmf	$$⊢\phi \to F\in \mathrm{SMblFn}\left(B\right)$$