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 \subseteq T \land T \subseteq ℂ) \to (x \in S ⟼ x) : S \underset{cn}{⟶} T$

Proof

Step	Hyp	Ref	Expression
1		cncfss	$⊢ (S \subseteq T \land T \subseteq ℂ) \to S \underset{cn}{⟶} S \subseteq S \underset{cn}{⟶} T$
2		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
3	2	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
4		sstr	$⊢ (S \subseteq T \land T \subseteq ℂ) \to S \subseteq ℂ$
5		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land S \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
6	3 4 5	sylancr	$⊢ (S \subseteq T \land T \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
7	6	cnmptid	$⊢ (S \subseteq T \land T \subseteq ℂ) \to (x \in S ⟼ x) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} S) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} S))$
8		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
9	2 8 8	cncfcn	$⊢ (S \subseteq ℂ \land S \subseteq ℂ) \to S \underset{cn}{⟶} S = (TopOpen (ℂ_{fld}) ↾_{𝑡} S) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
10	4 4 9	syl2anc	$⊢ (S \subseteq T \land T \subseteq ℂ) \to S \underset{cn}{⟶} S = (TopOpen (ℂ_{fld}) ↾_{𝑡} S) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
11	7 10	eleqtrrd	$⊢ (S \subseteq T \land T \subseteq ℂ) \to (x \in S ⟼ x) : S \underset{cn}{⟶} S$
12	1 11	sseldd	$⊢ (S \subseteq T \land T \subseteq ℂ) \to (x \in S ⟼ x) : S \underset{cn}{⟶} T$