Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cncfmptid Structured version   Visualization version   GIF version

Theorem cncfmptid 23619
 Description: The identity function is a continuous function on ℂ. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 17-May-2016.)
Assertion
Ref Expression
cncfmptid ((𝑆𝑇𝑇 ⊆ ℂ) → (𝑥𝑆𝑥) ∈ (𝑆cn𝑇))
Distinct variable groups:   𝑥,𝑆   𝑥,𝑇

Proof of Theorem cncfmptid
StepHypRef Expression
1 cncfss 23605 . 2 ((𝑆𝑇𝑇 ⊆ ℂ) → (𝑆cn𝑆) ⊆ (𝑆cn𝑇))
2 eqid 2758 . . . . . 6 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
32cnfldtopon 23489 . . . . 5 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
4 sstr 3902 . . . . 5 ((𝑆𝑇𝑇 ⊆ ℂ) → 𝑆 ⊆ ℂ)
5 resttopon 21866 . . . . 5 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
63, 4, 5sylancr 590 . . . 4 ((𝑆𝑇𝑇 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
76cnmptid 22366 . . 3 ((𝑆𝑇𝑇 ⊆ ℂ) → (𝑥𝑆𝑥) ∈ (((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld) ↾t 𝑆)))
8 eqid 2758 . . . . 5 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
92, 8, 8cncfcn 23616 . . . 4 ((𝑆 ⊆ ℂ ∧ 𝑆 ⊆ ℂ) → (𝑆cn𝑆) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld) ↾t 𝑆)))
104, 4, 9syl2anc 587 . . 3 ((𝑆𝑇𝑇 ⊆ ℂ) → (𝑆cn𝑆) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn ((TopOpen‘ℂfld) ↾t 𝑆)))
117, 10eleqtrrd 2855 . 2 ((𝑆𝑇𝑇 ⊆ ℂ) → (𝑥𝑆𝑥) ∈ (𝑆cn𝑆))
121, 11sseldd 3895 1 ((𝑆𝑇𝑇 ⊆ ℂ) → (𝑥𝑆𝑥) ∈ (𝑆cn𝑇))