Definition df-sconn 31204

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.)

Assertion

Ref	Expression
df-sconn	|- SConn = { j e. PConn | A. f e. ( II Cn j ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) }

Distinct variable group:   f, j

Detailed syntax breakdown of Definition df-sconn

Step	Hyp	Ref	Expression
1		csconn 31202	. 2 class SConn
2		cc0 9936	. . . . . . 7 class 0
3		vf	. . . . . . . 8 setvar f
4	3	cv 1482	. . . . . . 7 class f
5	2, 4	cfv 5888	. . . . . 6 class ( f ` 0 )
6		c1 9937	. . . . . . 7 class 1
7	6, 4	cfv 5888	. . . . . 6 class ( f ` 1 )
8	5, 7	wceq 1483	. . . . 5 wff ( f ` 0 ) = ( f ` 1 )
9		cicc 12178	. . . . . . . 8 class [,]
10	2, 6, 9	co 6650	. . . . . . 7 class ( 0 [,] 1 )
11	5	csn 4177	. . . . . . 7 class { ( f ` 0 ) }
12	10, 11	cxp 5112	. . . . . 6 class ( ( 0 [,] 1 ) X. { ( f ` 0 ) } )
13		vj	. . . . . . . 8 setvar j
14	13	cv 1482	. . . . . . 7 class j
15		cphtpc 22768	. . . . . . 7 class ~=ph
16	14, 15	cfv 5888	. . . . . 6 class ( ~=ph ` j )
17	4, 12, 16	wbr 4653	. . . . 5 wff f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } )
18	8, 17	wi 4	. . . 4 wff ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) )
19		cii 22678	. . . . 5 class II
20		ccn 21028	. . . . 5 class Cn
21	19, 14, 20	co 6650	. . . 4 class ( II Cn j )
22	18, 3, 21	wral 2912	. . 3 wff A. f e. ( II Cn j ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) )
23		cpconn 31201	. . 3 class PConn
24	22, 13, 23	crab 2916	. 2 class { j e. PConn | A. f e. ( II Cn j ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) }
25	1, 24	wceq 1483	1 wff SConn = { j e. PConn | A. f e. ( II Cn j ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) }

This definition is referenced by:  issconn  31208