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 (.)$

Step	Hyp	Ref	Expression
1		ioomax	$⊢ (−∞, +∞) = ℝ$
2		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
3		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
4	2 3	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
5		mnfxr	$⊢ −∞ \in ℝ^{*}$
6		pnfxr	$⊢ +∞ \in ℝ^{*}$
7		fnovrn	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land −∞ \in ℝ^{} \land +∞ \in ℝ^{}) \to (−∞, +∞) \in ran (.)$
8	4 5 6 7	mp3an	$⊢ (−∞, +∞) \in ran (.)$
9	1 8	eqeltrri	$⊢ ℝ \in ran (.)$
10		elssuni	$⊢ ℝ \in ran (.) \to ℝ \subseteq ⋃ ran (.)$
11	9 10	ax-mp	$⊢ ℝ \subseteq ⋃ ran (.)$
12		frn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to ran (.) \subseteq 𝒫 ℝ$
13	2 12	ax-mp	$⊢ ran (.) \subseteq 𝒫 ℝ$
14		sspwuni	$⊢ ran (.) \subseteq 𝒫 ℝ \leftrightarrow ⋃ ran (.) \subseteq ℝ$
15	13 14	mpbi	$⊢ ⋃ ran (.) \subseteq ℝ$
16	11 15	eqssi	$⊢ ℝ = ⋃ ran (.)$

Metamath Proof Explorer