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=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	fcnre.3	$$⊢T=\bigcup J$$
	sfcnre.5	$$⊢C=J\mathrm{Cn}K$$
	fcnre.6	$$⊢\phi \to F\in C$$
Assertion	fcnre	$$⊢\phi \to F:T⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		fcnre.1	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		fcnre.3	$$⊢T=\bigcup J$$
3		sfcnre.5	$$⊢C=J\mathrm{Cn}K$$
4		fcnre.6	$$⊢\phi \to F\in C$$
5	4 3	eleqtrdi	$$⊢\phi \to F\in \left(J\mathrm{Cn}K\right)$$
6		cntop1	$$⊢F\in \left(J\mathrm{Cn}K\right)\to J\in \mathrm{Top}$$
7	5 6	syl	$$⊢\phi \to J\in \mathrm{Top}$$
8	2	toptopon	$$⊢J\in \mathrm{Top}\leftrightarrow J\in \mathrm{TopOn}\left(T\right)$$
9	7 8	sylib	$$⊢\phi \to J\in \mathrm{TopOn}\left(T\right)$$
10		retopon	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$$
11	1 10	eqeltri	$$⊢K\in \mathrm{TopOn}\left(ℝ\right)$$
12	11	a1i	$$⊢\phi \to K\in \mathrm{TopOn}\left(ℝ\right)$$
13		cnf2	$$⊢\left(J\in \mathrm{TopOn}\left(T\right)\wedge K\in \mathrm{TopOn}\left(ℝ\right)\wedge F\in \left(J\mathrm{Cn}K\right)\right)\to F:T⟶ℝ$$
14	9 12 5 13	syl3anc	$$⊢\phi \to F:T⟶ℝ$$