iitopon

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

		Ref	Expression
	Assertion	iitopon	$⊢ II \in TopOn ([0, 1])$

Step	Hyp	Ref	Expression
1		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
2		unitssre	$⊢ [0, 1] \subseteq ℝ$
3		ax-resscn	$⊢ ℝ \subseteq ℂ$
4	2 3	sstri	$⊢ [0, 1] \subseteq ℂ$
5		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land [0, 1] \subseteq ℂ) \to {(abs \circ -) ↾}_{([0, 1] \times [0, 1])} \in ∞Met ([0, 1])$
6	1 4 5	mp2an	$⊢ {(abs \circ -) ↾}_{([0, 1] \times [0, 1])} \in ∞Met ([0, 1])$
7		df-ii	$⊢ II = MetOpen ({(abs \circ -) ↾}_{([0, 1] \times [0, 1])})$
8	7	mopntopon	$⊢ {(abs \circ -) ↾}_{([0, 1] \times [0, 1])} \in ∞Met ([0, 1]) \to II \in TopOn ([0, 1])$
9	6 8	ax-mp	$⊢ II \in TopOn ([0, 1])$

Metamath Proof Explorer