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 ⊢ A B ∈ ran ⁡ .

Proof

Step Hyp Ref Expression
1 id ⊢ A B = ∅ → A B = ∅
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 ⊢ A B = ∅ → A B ∈ ran ⁡ .
11 n0 ⊢ A B ≠ ∅ ↔ ∃ x x ∈ A B
12 eliooxr ⊢ x ∈ A B → A ∈ ℝ * ∧ B ∈ ℝ *
13 fnovrn ⊢ . Fn ℝ * × ℝ * ∧ A ∈ ℝ * ∧ B ∈ ℝ * → A B ∈ ran ⁡ .
14 5 13 mp3an1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A B ∈ ran ⁡ .
15 12 14 syl ⊢ x ∈ A B → A B ∈ ran ⁡ .
16 15 exlimiv ⊢ ∃ x x ∈ A B → A B ∈ ran ⁡ .
17 11 16 sylbi ⊢ A B ≠ ∅ → A B ∈ ran ⁡ .
18 10 17 pm2.61ine ⊢ A B ∈ ran ⁡ .