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 = U. J
sfcnre.5 
|- C = ( J Cn K )
fcnre.6 
|- ( ph -> F e. C )
Assertion fcnre 
|- ( ph -> F : T --> RR )

Proof

Step Hyp Ref Expression
1 fcnre.1 
 |-  K = ( topGen ` ran (,) )
2 fcnre.3 
 |-  T = U. J
3 sfcnre.5 
 |-  C = ( J Cn K )
4 fcnre.6 
 |-  ( ph -> F e. C )
5 4 3 eleqtrdi 
 |-  ( ph -> F e. ( J Cn K ) )
6 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
7 5 6 syl 
 |-  ( ph -> J e. Top )
8 2 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` T ) )
9 7 8 sylib 
 |-  ( ph -> J e. ( TopOn ` T ) )
10 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
11 1 10 eqeltri 
 |-  K e. ( TopOn ` RR )
12 11 a1i 
 |-  ( ph -> K e. ( TopOn ` RR ) )
13 cnf2 
 |-  ( ( J e. ( TopOn ` T ) /\ K e. ( TopOn ` RR ) /\ F e. ( J Cn K ) ) -> F : T --> RR )
14 9 12 5 13 syl3anc 
 |-  ( ph -> F : T --> RR )