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 ⊢ S ⊆ T ∧ T ⊆ ℂ → x ∈ S ⟼ x : S ⟶cn T

Proof

Step Hyp Ref Expression
1 cncfss ⊢ S ⊆ T ∧ T ⊆ ℂ → S ⟶cn S ⊆ S ⟶cn T
2 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
3 2 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
4 sstr ⊢ S ⊆ T ∧ T ⊆ ℂ → S ⊆ ℂ
5 resttopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ S ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 S ∈ TopOn ⁡ S
6 3 4 5 sylancr ⊢ S ⊆ T ∧ T ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 S ∈ TopOn ⁡ S
7 6 cnmptid ⊢ S ⊆ T ∧ T ⊆ ℂ → x ∈ S ⟼ x ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 S Cn TopOpen ⁡ ℂ fld ↾ 𝑡 S
8 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 S = TopOpen ⁡ ℂ fld ↾ 𝑡 S
9 2 8 8 cncfcn ⊢ S ⊆ ℂ ∧ S ⊆ ℂ → S ⟶cn S = TopOpen ⁡ ℂ fld ↾ 𝑡 S Cn TopOpen ⁡ ℂ fld ↾ 𝑡 S
10 4 4 9 syl2anc ⊢ S ⊆ T ∧ T ⊆ ℂ → S ⟶cn S = TopOpen ⁡ ℂ fld ↾ 𝑡 S Cn TopOpen ⁡ ℂ fld ↾ 𝑡 S
11 7 10 eleqtrrd ⊢ S ⊆ T ∧ T ⊆ ℂ → x ∈ S ⟼ x : S ⟶cn S
12 1 11 sseldd ⊢ S ⊆ T ∧ T ⊆ ℂ → x ∈ S ⟼ x : S ⟶cn T