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		unitsscn	⊢ ( 0 [,] 1 ) ⊆ ℂ
3		xmetres2	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ∞Met ‘ ( 0 [,] 1 ) ) )
4	1 2 3	mp2an	⊢ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ∞Met ‘ ( 0 [,] 1 ) )
5		df-ii	⊢ II = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
6	5	mopntopon	⊢ ( ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ∞Met ‘ ( 0 [,] 1 ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
7	4 6	ax-mp	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )