Theorem ioorebas

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

	Ref	Expression
Assertion	ioorebas	⊢ ( 𝐴 (,) 𝐵 ) ∈ ran (,)

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ( 𝐴 (,) 𝐵 ) = ∅ → ( 𝐴 (,) 𝐵 ) = ∅ )
2		iooid	⊢ ( 0 (,) 0 ) = ∅
3		ioof	⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
4		ffn	⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
5	3 4	ax-mp	⊢ (,) Fn ( ℝ* × ℝ* )
6		0xr	⊢ 0 ∈ ℝ*
7		fnovrn	⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ 0 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 0 (,) 0 ) ∈ ran (,) )
8	5 6 6 7	mp3an	⊢ ( 0 (,) 0 ) ∈ ran (,)
9	2 8	eqeltrri	⊢ ∅ ∈ ran (,)
10	1 9	eqeltrdi	⊢ ( ( 𝐴 (,) 𝐵 ) = ∅ → ( 𝐴 (,) 𝐵 ) ∈ ran (,) )
11		n0	⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
12		eliooxr	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
13		fnovrn	⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) ∈ ran (,) )
14	5 13	mp3an1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) ∈ ran (,) )
15	12 14	syl	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 (,) 𝐵 ) ∈ ran (,) )
16	15	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 (,) 𝐵 ) ∈ ran (,) )
17	11 16	sylbi	⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐴 (,) 𝐵 ) ∈ ran (,) )
18	10 17	pm2.61ine	⊢ ( 𝐴 (,) 𝐵 ) ∈ ran (,)