Metamath Proof Explorer

Theorem issconn

Description: The property of being a simply connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion issconn ⊢ J ∈ SConn ↔ J ∈ PConn ∧ ∀ f ∈ II Cn J f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ J 0 1 × f ⁡ 0

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ j = J → II Cn j = II Cn J
2 fveq2 ⊢ j = J → ≃ ph ⁡ j = ≃ ph ⁡ J
3 2 breqd ⊢ j = J → f ≃ ph ⁡ j 0 1 × f ⁡ 0 ↔ f ≃ ph ⁡ J 0 1 × f ⁡ 0
4 3 imbi2d ⊢ j = J → f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ j 0 1 × f ⁡ 0 ↔ f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ J 0 1 × f ⁡ 0
5 1 4 raleqbidv ⊢ j = J → ∀ f ∈ II Cn j f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ j 0 1 × f ⁡ 0 ↔ ∀ f ∈ II Cn J f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ J 0 1 × f ⁡ 0
6 df-sconn ⊢ SConn = j ∈ PConn | ∀ f ∈ II Cn j f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ j 0 1 × f ⁡ 0
7 5 6 elrab2 ⊢ J ∈ SConn ↔ J ∈ PConn ∧ ∀ f ∈ II Cn J f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ J 0 1 × f ⁡ 0