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 ⊢ K = topGen ⁡ ran ⁡ .
fcnre.3 ⊢ T = ⋃ J
sfcnre.5 ⊢ C = J Cn K
fcnre.6 ⊢ φ → F ∈ C
Assertion fcnre ⊢ φ → F : T ⟶ ℝ

Proof

Step Hyp Ref Expression
1 fcnre.1 ⊢ K = topGen ⁡ ran ⁡ .
2 fcnre.3 ⊢ T = ⋃ J
3 sfcnre.5 ⊢ C = J Cn K
4 fcnre.6 ⊢ φ → F ∈ C
5 4 3 eleqtrdi ⊢ φ → F ∈ J Cn K
6 cntop1 ⊢ F ∈ J Cn K → J ∈ Top
7 5 6 syl ⊢ φ → J ∈ Top
8 2 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ T
9 7 8 sylib ⊢ φ → J ∈ TopOn ⁡ T
10 retopon ⊢ topGen ⁡ ran ⁡ . ∈ TopOn ⁡ ℝ
11 1 10 eqeltri ⊢ K ∈ TopOn ⁡ ℝ
12 11 a1i ⊢ φ → K ∈ TopOn ⁡ ℝ
13 cnf2 ⊢ J ∈ TopOn ⁡ T ∧ K ∈ TopOn ⁡ ℝ ∧ F ∈ J Cn K → F : T ⟶ ℝ
14 9 12 5 13 syl3anc ⊢ φ → F : T ⟶ ℝ