iccordt

Description: A closed interval is closed in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Assertion	iccordt	$⊢ [A, B] \in Clsd (ordTop (\leq))$

Step	Hyp	Ref	Expression
1		df-ov	$⊢ [A, B] = [.] (⟨A, B⟩)$
2		letsr	$⊢ \leq \in TosetRel$
3		ledm	$⊢ ℝ^{*} = dom \leq$
4	3	ordtcld3	$⊢ (\leq \in TosetRel \land x \in ℝ^{} \land y \in ℝ^{}) \to \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\} \in Clsd (ordTop (\leq))$
5	2 4	mp3an1	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\} \in Clsd (ordTop (\leq))$
6	5	rgen2	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\} \in Clsd (ordTop (\leq))$
7		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\})$
8	7	fmpo	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} \{z \in ℝ^{} \| (x \leq z \land z \leq y)\} \in Clsd (ordTop (\leq)) \leftrightarrow [.] : ℝ^{} \times ℝ^{*} ⟶ Clsd (ordTop (\leq))$
9	6 8	mpbi	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ Clsd (ordTop (\leq))$
10		letop	$⊢ ordTop (\leq) \in Top$
11		0cld	$⊢ ordTop (\leq) \in Top \to \emptyset \in Clsd (ordTop (\leq))$
12	10 11	ax-mp	$⊢ \emptyset \in Clsd (ordTop (\leq))$
13	9 12	f0cli	$⊢ [.] (⟨A, B⟩) \in Clsd (ordTop (\leq))$
14	1 13	eqeltri	$⊢ [A, B] \in Clsd (ordTop (\leq))$

Metamath Proof Explorer