Theorem iitopon

Description: The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	iitopon	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )

Proof

Step	Hyp	Ref	Expression
1		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
2		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
3		ax-resscn	⊢ ℝ ⊆ ℂ
4	2 3	sstri	⊢ ( 0 [,] 1 ) ⊆ ℂ
5		xmetres2	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ∞Met ‘ ( 0 [,] 1 ) ) )
6	1 4 5	mp2an	⊢ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ∞Met ‘ ( 0 [,] 1 ) )
7		df-ii	⊢ II = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
8	7	mopntopon	⊢ ( ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ∞Met ‘ ( 0 [,] 1 ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
9	6 8	ax-mp	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )