Theorem ioosconn

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

	Ref	Expression
Assertion	ioosconn	⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ SConn

Proof

Step	Hyp	Ref	Expression
1		iccssioo2	⊢ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 (,) 𝐵 ) )
2	1	rgen2	⊢ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 (,) 𝐵 )
3		ioossre	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
4		eqid	⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,) 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,) 𝐵 ) )
5	4	resconn	⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ SConn ↔ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ Conn ) )
6		reconn	⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ Conn ↔ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 (,) 𝐵 ) ) )
7	5 6	bitr2d	⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ → ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 (,) 𝐵 ) ↔ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ SConn ) )
8	3 7	ax-mp	⊢ ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐴 (,) 𝐵 ) ↔ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ SConn )
9	2 8	mpbi	⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 (,) 𝐵 ) ) ∈ SConn