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 )