Theorem retopconn

Description: Corollary of reconn . The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009)

	Ref	Expression
Assertion	retopconn	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Conn}$$

Proof

Step	Hyp	Ref	Expression
1		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
2		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3	2	restid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}ℝ=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
4	1 3	ax-mp	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}ℝ=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
5		iccssre	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left[x,y\right]\subseteq ℝ$$
6	5	rgen2	$$⊢\forall x\in ℝ\forall y\in ℝ\left[x,y\right]\subseteq ℝ$$
7		ssid	$$⊢ℝ\subseteq ℝ$$
8		reconn	$$⊢ℝ\subseteq ℝ\to \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}ℝ\in \mathrm{Conn}\leftrightarrow \forall x\in ℝ\forall y\in ℝ\left[x,y\right]\subseteq ℝ\right)$$
9	7 8	ax-mp	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}ℝ\in \mathrm{Conn}\leftrightarrow \forall x\in ℝ\forall y\in ℝ\left[x,y\right]\subseteq ℝ$$
10	6 9	mpbir	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}ℝ\in \mathrm{Conn}$$
11	4 10	eqeltrri	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Conn}$$