Theorem abscncfALT

Description: Absolute value is continuous. Alternate proof of abscncf . (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	abscncfALT	$$⊢\mathrm{abs}:ℂ\underset{cn}{⟶}ℝ$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3	1 2	abscn	$$⊢\mathrm{abs}\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
4		ssid	$$⊢ℂ\subseteq ℂ$$
5		ax-resscn	$$⊢ℝ\subseteq ℂ$$
6	1	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
7	6	toponunii	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
8	7	restid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
9	6 8	ax-mp	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
10	9	eqcomi	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
11	1	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
12	1 10 11	cncfcn	$$⊢\left(ℂ\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to ℂ\underset{cn}{⟶}ℝ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
13	4 5 12	mp2an	$$⊢ℂ\underset{cn}{⟶}ℝ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
14	3 13	eleqtrri	$$⊢\mathrm{abs}:ℂ\underset{cn}{⟶}ℝ$$