retopconn

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

		Ref	Expression
	Assertion	retopconn	$⊢ topGen (ran (.)) \in Conn$

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

Metamath Proof Explorer