Theorem fcnre

Description: A function continuous with respect to the standard topology, is a real mapping. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	fcnre.1	⊢ 𝐾 = ( topGen ‘ ran (,) )
	fcnre.3	⊢ 𝑇 = ∪ 𝐽
	sfcnre.5	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
	fcnre.6	⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
Assertion	fcnre	⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		fcnre.1	⊢ 𝐾 = ( topGen ‘ ran (,) )
2		fcnre.3	⊢ 𝑇 = ∪ 𝐽
3		sfcnre.5	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
4		fcnre.6	⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
5	4 3	eleqtrdi	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
6		cntop1	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
7	5 6	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
8	2	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑇 ) )
9	7 8	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑇 ) )
10		retopon	⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
11	1 10	eqeltri	⊢ 𝐾 ∈ ( TopOn ‘ ℝ )
12	11	a1i	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ℝ ) )
13		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑇 ) ∧ 𝐾 ∈ ( TopOn ‘ ℝ ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝑇 ⟶ ℝ )
14	9 12 5 13	syl3anc	⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )