iccconn

Description: A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009)

		Ref	Expression
	Assertion	iccconn	$⊢ (A \in ℝ \land B \in ℝ) \to topGen (ran (.)) ↾_{𝑡} [A, B] \in Conn$

Step	Hyp	Ref	Expression
1		iccss2	$⊢ (x \in [A, B] \land y \in [A, B]) \to [x, y] \subseteq [A, B]$
2	1	rgen2	$⊢ \forall x \in [A, B] \forall y \in [A, B] [x, y] \subseteq [A, B]$
3		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
4		reconn	$⊢ [A, B] \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} [A, B] \in Conn \leftrightarrow \forall x \in [A, B] \forall y \in [A, B] [x, y] \subseteq [A, B])$
5	3 4	syl	$⊢ (A \in ℝ \land B \in ℝ) \to (topGen (ran (.)) ↾_{𝑡} [A, B] \in Conn \leftrightarrow \forall x \in [A, B] \forall y \in [A, B] [x, y] \subseteq [A, B])$
6	2 5	mpbiri	$⊢ (A \in ℝ \land B \in ℝ) \to topGen (ran (.)) ↾_{𝑡} [A, B] \in Conn$

Metamath Proof Explorer