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

Proof

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