Theorem dfii3

Description: Alternate definition of the unit interval. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypothesis	dfii3.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	dfii3	$$⊢\mathrm{II}=J{\upharpoonright }_{𝑡}\left[0,1\right]$$

Proof

Step	Hyp	Ref	Expression
1		dfii3.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		cnxmet	$$⊢\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$$
3		unitssre	$$⊢\left[0,1\right]\subseteq ℝ$$
4		ax-resscn	$$⊢ℝ\subseteq ℂ$$
5	3 4	sstri	$$⊢\left[0,1\right]\subseteq ℂ$$
6		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(\left[0,1\right]\times \left[0,1\right]\right)}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(\left[0,1\right]\times \left[0,1\right]\right)}$$
7	1	cnfldtopn	$$⊢J=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$$
8		df-ii	$$⊢\mathrm{II}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(\left[0,1\right]\times \left[0,1\right]\right)}\right)$$
9	6 7 8	metrest	$$⊢\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge \left[0,1\right]\subseteq ℂ\right)\to J{\upharpoonright }_{𝑡}\left[0,1\right]=\mathrm{II}$$
10	2 5 9	mp2an	$$⊢J{\upharpoonright }_{𝑡}\left[0,1\right]=\mathrm{II}$$
11	10	eqcomi	$$⊢\mathrm{II}=J{\upharpoonright }_{𝑡}\left[0,1\right]$$