ioorebas

Description: Open intervals are elements of the set of all open intervals. (Contributed by Mario Carneiro, 26-Mar-2015)

		Ref	Expression
	Assertion	ioorebas	$⊢ (A, B) \in ran (.)$

Step	Hyp	Ref	Expression
1		id	$⊢ (A, B) = \emptyset \to (A, B) = \emptyset$
2		iooid	$⊢ (0, 0) = \emptyset$
3		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
4		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
5	3 4	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
6		0xr	$⊢ 0 \in ℝ^{*}$
7		fnovrn	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land 0 \in ℝ^{} \land 0 \in ℝ^{}) \to (0, 0) \in ran (.)$
8	5 6 6 7	mp3an	$⊢ (0, 0) \in ran (.)$
9	2 8	eqeltrri	$⊢ \emptyset \in ran (.)$
10	1 9	eqeltrdi	$⊢ (A, B) = \emptyset \to (A, B) \in ran (.)$
11		n0	$⊢ (A, B) \neq \emptyset \leftrightarrow \exists x x \in (A, B)$
12		eliooxr	$⊢ x \in (A, B) \to (A \in ℝ^{} \land B \in ℝ^{})$
13		fnovrn	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) \in ran (.)$
14	5 13	mp3an1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) \in ran (.)$
15	12 14	syl	$⊢ x \in (A, B) \to (A, B) \in ran (.)$
16	15	exlimiv	$⊢ \exists x x \in (A, B) \to (A, B) \in ran (.)$
17	11 16	sylbi	$⊢ (A, B) \neq \emptyset \to (A, B) \in ran (.)$
18	10 17	pm2.61ine	$⊢ (A, B) \in ran (.)$

Metamath Proof Explorer