icccldii

		Ref	Expression
	Assertion	icccldii	$⊢ (0 \leq A \land B \leq 1) \to [A, B] \in Clsd (II)$

Step	Hyp	Ref	Expression
1		iccssxr	$⊢ [0, 1] \subseteq ℝ^{*}$
2		iccordt	$⊢ [A, B] \in Clsd (ordTop (\leq))$
3		0re	$⊢ 0 \in ℝ$
4		1re	$⊢ 1 \in ℝ$
5		iccss	$⊢ ((0 \in ℝ \land 1 \in ℝ) \land (0 \leq A \land B \leq 1)) \to [A, B] \subseteq [0, 1]$
6	3 4 5	mpanl12	$⊢ (0 \leq A \land B \leq 1) \to [A, B] \subseteq [0, 1]$
7		letopuni	$⊢ ℝ^{*} = ⋃ ordTop (\leq)$
8	7	restcldi	$⊢ ([0, 1] \subseteq ℝ^{*} \land [A, B] \in Clsd (ordTop (\leq)) \land [A, B] \subseteq [0, 1]) \to [A, B] \in Clsd (ordTop (\leq) ↾_{𝑡} [0, 1])$
9	1 2 6 8	mp3an12i	$⊢ (0 \leq A \land B \leq 1) \to [A, B] \in Clsd (ordTop (\leq) ↾_{𝑡} [0, 1])$
10		dfii5	$⊢ II = ordTop (\leq \cap ([0, 1] \times [0, 1]))$
11		ordtresticc	$⊢ ordTop (\leq) ↾_{𝑡} [0, 1] = ordTop (\leq \cap ([0, 1] \times [0, 1]))$
12	10 11	eqtr4i	$⊢ II = ordTop (\leq) ↾_{𝑡} [0, 1]$
13	12	fveq2i	$⊢ Clsd (II) = Clsd (ordTop (\leq) ↾_{𝑡} [0, 1])$
14	9 13	eleqtrrdi	$⊢ (0 \leq A \land B \leq 1) \to [A, B] \in Clsd (II)$

Metamath Proof Explorer