This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (,)