Metamath Proof Explorer

Definition df-sconn

Description: Define the class of simply connected topologies. A topology is simply connected if it is path-connected and every loop (continuous path with identical start and endpoint) is contractible to a point (path-homotopic to a constant function). (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion df-sconn ⊢ SConn = j ∈ PConn | ∀ f ∈ II Cn j f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ j 0 1 × f ⁡ 0

Detailed syntax breakdown

Step Hyp Ref Expression
0 csconn class SConn
1 vj setvar j
2 cpconn class PConn
3 vf setvar f
4 cii class II
5 ccn class Cn
6 1 cv setvar j
7 4 6 5 co class II Cn j
8 3 cv setvar f
9 cc0 class 0
10 9 8 cfv class f ⁡ 0
11 c1 class 1
12 11 8 cfv class f ⁡ 1
13 10 12 wceq wff f ⁡ 0 = f ⁡ 1
14 cphtpc class ≃ ph
15 6 14 cfv class ≃ ph ⁡ j
16 cicc class .
17 9 11 16 co class 0 1
18 10 csn class f ⁡ 0
19 17 18 cxp class 0 1 × f ⁡ 0
20 8 19 15 wbr wff f ≃ ph ⁡ j 0 1 × f ⁡ 0
21 13 20 wi wff f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ j 0 1 × f ⁡ 0
22 21 3 7 wral wff ∀ f ∈ II Cn j f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ j 0 1 × f ⁡ 0
23 22 1 2 crab class j ∈ PConn | ∀ f ∈ II Cn j f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ j 0 1 × f ⁡ 0
24 0 23 wceq wff SConn = j ∈ PConn | ∀ f ∈ II Cn j f ⁡ 0 = f ⁡ 1 → f ≃ ph ⁡ j 0 1 × f ⁡ 0