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		unitsscn	$$⊢\left[0,1\right]\subseteq ℂ$$
4		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)}$$
5	1	cnfldtopn	$$⊢J=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$$
6		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)$$
7	4 5 6	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}$$
8	2 3 7	mp2an	$$⊢J{\upharpoonright }_{𝑡}\left[0,1\right]=\mathrm{II}$$
9	8	eqcomi	$$⊢\mathrm{II}=J{\upharpoonright }_{𝑡}\left[0,1\right]$$