iooii

Description: Open intervals are open sets of II . (Contributed by Zhi Wang, 9-Sep-2024)

		Ref	Expression
	Assertion	iooii	$⊢ (0 \leq A \land B \leq 1) \to (A, B) \in II$

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		1xr	$⊢ 1 \in ℝ^{*}$
3		ioossioo	$⊢ ((0 \in ℝ^{} \land 1 \in ℝ^{}) \land (0 \leq A \land B \leq 1)) \to (A, B) \subseteq (0, 1)$
4	1 2 3	mpanl12	$⊢ (0 \leq A \land B \leq 1) \to (A, B) \subseteq (0, 1)$
5		iooretop	$⊢ (A, B) \in topGen (ran (.))$
6		iooretop	$⊢ (0, 1) \in topGen (ran (.))$
7		ioossicc	$⊢ (0, 1) \subseteq [0, 1]$
8		retop	$⊢ topGen (ran (.)) \in Top$
9		ovex	$⊢ [0, 1] \in V$
10		restopnb	$⊢ ((topGen (ran (.)) \in Top \land [0, 1] \in V) \land ((0, 1) \in topGen (ran (.)) \land (0, 1) \subseteq [0, 1] \land (A, B) \subseteq (0, 1))) \to ((A, B) \in topGen (ran (.)) \leftrightarrow (A, B) \in (topGen (ran (.)) ↾_{𝑡} [0, 1]))$
11	8 9 10	mpanl12	$⊢ ((0, 1) \in topGen (ran (.)) \land (0, 1) \subseteq [0, 1] \land (A, B) \subseteq (0, 1)) \to ((A, B) \in topGen (ran (.)) \leftrightarrow (A, B) \in (topGen (ran (.)) ↾_{𝑡} [0, 1]))$
12	6 7 11	mp3an12	$⊢ (A, B) \subseteq (0, 1) \to ((A, B) \in topGen (ran (.)) \leftrightarrow (A, B) \in (topGen (ran (.)) ↾_{𝑡} [0, 1]))$
13	5 12	mpbii	$⊢ (A, B) \subseteq (0, 1) \to (A, B) \in (topGen (ran (.)) ↾_{𝑡} [0, 1])$
14		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
15	13 14	eleqtrrdi	$⊢ (A, B) \subseteq (0, 1) \to (A, B) \in II$
16	4 15	syl	$⊢ (0 \leq A \land B \leq 1) \to (A, B) \in II$

Metamath Proof Explorer