This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )