# Metamath Proof Explorer

## 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){↾}_{𝑡}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
9 6 8 ax-mp ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
10 9 eqcomi ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℂ$
11 1 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
12 1 10 11 cncfcn
13 4 5 12 mp2an
14 3 13 eleqtrri ${⊢}\mathrm{abs}:ℂ\underset{cn}{⟶}ℝ$