Theorem dfii2

Description: Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	dfii2	$$⊢\mathrm{II}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left[0,1\right]$$

Proof

Step	Hyp	Ref	Expression
1		unitssre	$$⊢\left[0,1\right]\subseteq ℝ$$
2		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3		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)$$
4	2 3	resubmet	$$⊢\left[0,1\right]\subseteq ℝ\to \mathrm{II}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left[0,1\right]$$
5	1 4	ax-mp	$$⊢\mathrm{II}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left[0,1\right]$$