Metamath Proof Explorer

Theorem ioosconn

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

Ref Expression
Assertion ioosconn ⊢ topGen ⁡ ran ⁡ . ↾ 𝑡 A B ∈ SConn

Proof

Step Hyp Ref Expression
1 iccssioo2 ⊢ x ∈ A B ∧ y ∈ A B → x y ⊆ A B
2 1 rgen2 ⊢ ∀ x ∈ A B ∀ y ∈ A B x y ⊆ A B
3 ioossre ⊢ A B ⊆ ℝ
4 eqid ⊢ topGen ⁡ ran ⁡ . ↾ 𝑡 A B = topGen ⁡ ran ⁡ . ↾ 𝑡 A B
5 4 resconn ⊢ A B ⊆ ℝ → topGen ⁡ ran ⁡ . ↾ 𝑡 A B ∈ SConn ↔ topGen ⁡ ran ⁡ . ↾ 𝑡 A B ∈ Conn
6 reconn ⊢ A B ⊆ ℝ → topGen ⁡ ran ⁡ . ↾ 𝑡 A B ∈ Conn ↔ ∀ x ∈ A B ∀ y ∈ A B x y ⊆ A B
7 5 6 bitr2d ⊢ A B ⊆ ℝ → ∀ x ∈ A B ∀ y ∈ A B x y ⊆ A B ↔ topGen ⁡ ran ⁡ . ↾ 𝑡 A B ∈ SConn
8 3 7 ax-mp ⊢ ∀ x ∈ A B ∀ y ∈ A B x y ⊆ A B ↔ topGen ⁡ ran ⁡ . ↾ 𝑡 A B ∈ SConn
9 2 8 mpbi ⊢ topGen ⁡ ran ⁡ . ↾ 𝑡 A B ∈ SConn