Theorem icoreunrn

Description: The union of all closed-below, open-above intervals of reals is the set of reals. (Contributed by ML, 27-Jul-2020)

	Ref	Expression
Hypothesis	icoreunrn.1	$$⊢I=\left[.\right)\left[{ℝ}^2\right]$$
Assertion	icoreunrn	$$⊢ℝ=\bigcup I$$

Proof

Step	Hyp	Ref	Expression
1		icoreunrn.1	$$⊢I=\left[.\right)\left[{ℝ}^2\right]$$
2		rexr	$$⊢x\in ℝ\to x\in {ℝ}^{*}$$
3		peano2re	$$⊢x\in ℝ\to x+1\in ℝ$$
4		rexr	$$⊢x+1\in ℝ\to x+1\in {ℝ}^{*}$$
5	3 4	syl	$$⊢x\in ℝ\to x+1\in {ℝ}^{*}$$
6		ltp1	$$⊢x\in ℝ\to x<x+1$$
7		lbico1	$$⊢\left(x\in {ℝ}^{*}\wedge x+1\in {ℝ}^{*}\wedge x<x+1\right)\to x\in \left[x,x+1\right)$$
8	2 5 6 7	syl3anc	$$⊢x\in ℝ\to x\in \left[x,x+1\right)$$
9		df-ov	$$⊢\left[x,x+1\right)=\left[.\right)\left(⟨x,x+1⟩\right)$$
10	8 9	eleqtrdi	$$⊢x\in ℝ\to x\in \left[.\right)\left(⟨x,x+1⟩\right)$$
11		opelxpi	$$⊢\left(x\in ℝ\wedge x+1\in ℝ\right)\to ⟨x,x+1⟩\in {ℝ}^2$$
12	3 11	mpdan	$$⊢x\in ℝ\to ⟨x,x+1⟩\in {ℝ}^2$$
13		fvres	$$⊢⟨x,x+1⟩\in {ℝ}^2\to \left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨x,x+1⟩\right)=\left[.\right)\left(⟨x,x+1⟩\right)$$
14	12 13	syl	$$⊢x\in ℝ\to \left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨x,x+1⟩\right)=\left[.\right)\left(⟨x,x+1⟩\right)$$
15	10 14	eleqtrrd	$$⊢x\in ℝ\to x\in \left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨x,x+1⟩\right)$$
16		icoreresf	$$⊢\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right):{ℝ}^2⟶𝒫ℝ$$
17	16	fdmi	$$⊢\mathrm{dom}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)={ℝ}^2$$
18	11 17	eleqtrrdi	$$⊢\left(x\in ℝ\wedge x+1\in ℝ\right)\to ⟨x,x+1⟩\in \mathrm{dom}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)$$
19	3 18	mpdan	$$⊢x\in ℝ\to ⟨x,x+1⟩\in \mathrm{dom}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)$$
20		ffun	$$⊢\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right):{ℝ}^2⟶𝒫ℝ\to \mathrm{Fun}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)$$
21	16 20	ax-mp	$$⊢\mathrm{Fun}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)$$
22		fvelrn	$$⊢\left(\mathrm{Fun}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\wedge ⟨x,x+1⟩\in \mathrm{dom}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\right)\to \left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨x,x+1⟩\right)\in \mathrm{ran}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)$$
23	21 22	mpan	$$⊢⟨x,x+1⟩\in \mathrm{dom}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\to \left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨x,x+1⟩\right)\in \mathrm{ran}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)$$
24		df-ima	$$⊢\left[.\right)\left[{ℝ}^2\right]=\mathrm{ran}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)$$
25	1 24	eqtri	$$⊢I=\mathrm{ran}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)$$
26	23 25	eleqtrrdi	$$⊢⟨x,x+1⟩\in \mathrm{dom}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\to \left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨x,x+1⟩\right)\in I$$
27	19 26	syl	$$⊢x\in ℝ\to \left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨x,x+1⟩\right)\in I$$
28		elunii	$$⊢\left(x\in \left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨x,x+1⟩\right)\wedge \left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨x,x+1⟩\right)\in I\right)\to x\in \bigcup I$$
29	15 27 28	syl2anc	$$⊢x\in ℝ\to x\in \bigcup I$$
30	29	ssriv	$$⊢ℝ\subseteq \bigcup I$$
31		frn	$$⊢\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right):{ℝ}^2⟶𝒫ℝ\to \mathrm{ran}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\subseteq 𝒫ℝ$$
32	16 31	ax-mp	$$⊢\mathrm{ran}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\subseteq 𝒫ℝ$$
33	25 32	eqsstri	$$⊢I\subseteq 𝒫ℝ$$
34		uniss	$$⊢I\subseteq 𝒫ℝ\to \bigcup I\subseteq \bigcup 𝒫ℝ$$
35		unipw	$$⊢\bigcup 𝒫ℝ=ℝ$$
36	34 35	sseqtrdi	$$⊢I\subseteq 𝒫ℝ\to \bigcup I\subseteq ℝ$$
37	33 36	ax-mp	$$⊢\bigcup I\subseteq ℝ$$
38	30 37	eqssi	$$⊢ℝ=\bigcup I$$