This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ abs : ℂ ⟶cn ℝ

Proof

Step Hyp Ref Expression
1 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
2 eqid ⊢ topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ .
3 1 2 abscn ⊢ abs ∈ TopOpen ⁡ ℂ fld Cn topGen ⁡ ran ⁡ .
4 ssid ⊢ ℂ ⊆ ℂ
5 ax-resscn ⊢ ℝ ⊆ ℂ
6 1 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
7 6 toponunii ⊢ ℂ = ⋃ TopOpen ⁡ ℂ fld
8 7 restid ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ = TopOpen ⁡ ℂ fld
9 6 8 ax-mp ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ = TopOpen ⁡ ℂ fld
10 9 eqcomi ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
11 1 tgioo2 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
12 1 10 11 cncfcn ⊢ ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ → ℂ ⟶cn ℝ = TopOpen ⁡ ℂ fld Cn topGen ⁡ ran ⁡ .
13 4 5 12 mp2an ⊢ ℂ ⟶cn ℝ = TopOpen ⁡ ℂ fld Cn topGen ⁡ ran ⁡ .
14 3 13 eleqtrri ⊢ abs : ℂ ⟶cn ℝ