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→ ℝ )