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	$$⊢ℝ=\bigcup \mathrm{ran}\left(.\right)$$

Proof

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