ioosconn

Description: An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015)

		Ref	Expression
	Assertion	ioosconn	$⊢ topGen (ran (.)) ↾_{𝑡} (A, B) \in SConn$

Step	Hyp	Ref	Expression
1		iccssioo2	$⊢ (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		ioossre	$⊢ (A, B) \subseteq ℝ$
4		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} (A, B) = topGen (ran (.)) ↾_{𝑡} (A, B)$
5	4	resconn	$⊢ (A, B) \subseteq ℝ \to (topGen (ran (.)) ↾_{𝑡} (A, B) \in SConn \leftrightarrow topGen (ran (.)) ↾_{𝑡} (A, B) \in Conn)$
6		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))$
7	5 6	bitr2d	$⊢ (A, B) \subseteq ℝ \to (\forall x \in (A, B) \forall y \in (A, B) [x, y] \subseteq (A, B) \leftrightarrow topGen (ran (.)) ↾_{𝑡} (A, B) \in SConn)$
8	3 7	ax-mp	$⊢ \forall x \in (A, B) \forall y \in (A, B) [x, y] \subseteq (A, B) \leftrightarrow topGen (ran (.)) ↾_{𝑡} (A, B) \in SConn$
9	2 8	mpbi	$⊢ topGen (ran (.)) ↾_{𝑡} (A, B) \in SConn$

Metamath Proof Explorer