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

Metamath Proof Explorer

Theorem cncfmptid

Description: The identity function is a continuous function on CC . (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion cncfmptid ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝑥 ) ∈ ( 𝑆 –cn→ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 cncfss ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑆 –cn→ 𝑆 ) ⊆ ( 𝑆 –cn→ 𝑇 ) )
2 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3 2 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
4 sstr ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → 𝑆 ⊆ ℂ )
5 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
6 3 4 5 sylancr ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
7 6 cnmptid ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝑥 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) )
8 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
9 2 8 8 cncfcn ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝑆 ⊆ ℂ ) → ( 𝑆 –cn→ 𝑆 ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) )
10 4 4 9 syl2anc ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑆 –cn→ 𝑆 ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) )
11 7 10 eleqtrrd ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝑥 ) ∈ ( 𝑆 –cn→ 𝑆 ) )
12 1 11 sseldd ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑥 ∈ 𝑆 ↦ 𝑥 ) ∈ ( 𝑆 –cn→ 𝑇 ) )