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

Metamath Proof Explorer

Theorem unirnioo

Description: The union of the range of the open interval function. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 30-Jan-2014)

Ref Expression
Assertion unirnioo ℝ = ∪ ran (,)

Proof

Step Hyp Ref Expression
1 ioomax ⊢ ( -∞ (,) +∞ ) = ℝ
2 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
3 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
4 2 3 ax-mp ⊢ (,) Fn ( ℝ* × ℝ* )
5 mnfxr ⊢ -∞ ∈ ℝ*
6 pnfxr ⊢ +∞ ∈ ℝ*
7 fnovrn ⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ -∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -∞ (,) +∞ ) ∈ ran (,) )
8 4 5 6 7 mp3an ⊢ ( -∞ (,) +∞ ) ∈ ran (,)
9 1 8 eqeltrri ⊢ ℝ ∈ ran (,)
10 elssuni ⊢ ( ℝ ∈ ran (,) → ℝ ⊆ ∪ ran (,) )
11 9 10 ax-mp ⊢ ℝ ⊆ ∪ ran (,)
12 frn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → ran (,) ⊆ 𝒫 ℝ )
13 2 12 ax-mp ⊢ ran (,) ⊆ 𝒫 ℝ
14 sspwuni ⊢ ( ran (,) ⊆ 𝒫 ℝ ↔ ∪ ran (,) ⊆ ℝ )
15 13 14 mpbi ⊢ ∪ ran (,) ⊆ ℝ
16 11 15 eqssi ⊢ ℝ = ∪ ran (,)