Theorem retopsconn

Description: The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
2		ioomax	$$⊢\left(\mathrm{-\infty },\mathrm{+\infty }\right)=ℝ$$
3		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
4	2 3	eqtri	$$⊢\left(\mathrm{-\infty },\mathrm{+\infty }\right)=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
5	4	restid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left(\mathrm{-\infty },\mathrm{+\infty }\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
6	1 5	ax-mp	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left(\mathrm{-\infty },\mathrm{+\infty }\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
7		ioosconn	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left(\mathrm{-\infty },\mathrm{+\infty }\right)\in \mathrm{SConn}$$
8	6 7	eqeltrri	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{SConn}$$