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