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 ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
9 6 8 ax-mp ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
10 9 eqcomi ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
11 1 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
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→ ℝ )