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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	cnfrrnsmf.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) )
	cnfrrnsmf.k	⊢ 𝐾 = ( topGen ‘ ran (,) )
	cnfrrnsmf.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ↾t dom 𝐹 ) Cn 𝐾 ) )
	cnfrrnsmf.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
Assertion	cnfrrnsmf	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cnfrrnsmf.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		cnfrrnsmf.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) )
3		cnfrrnsmf.k	⊢ 𝐾 = ( topGen ‘ ran (,) )
4		cnfrrnsmf.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ↾t dom 𝐹 ) Cn 𝐾 ) )
5		cnfrrnsmf.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
6	2	rrxtop	⊢ ( 𝑋 ∈ Fin → 𝐽 ∈ Top )
7	1 6	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
8	7 3 4 5	cnfsmf	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝐵 ) )