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