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