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 e. PConn | A. f e. ( II Cn j ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csconn	|- SConn
1		vj	|- j
2		cpconn	|- PConn
3		vf	|- f
4		cii	|- II
5		ccn	|- Cn
6	1	cv	|- j
7	4 6 5	co	|- ( II Cn j )
8	3	cv	|- f
9		cc0	|- 0
10	9 8	cfv	|- ( f ` 0 )
11		c1	|- 1
12	11 8	cfv	|- ( f ` 1 )
13	10 12	wceq	|- ( f ` 0 ) = ( f ` 1 )
14		cphtpc	|- ~=ph
15	6 14	cfv	|- ( ~=ph ` j )
16		cicc	|- [,]
17	9 11 16	co	|- ( 0 [,] 1 )
18	10	csn	|- { ( f ` 0 ) }
19	17 18	cxp	|- ( ( 0 [,] 1 ) X. { ( f ` 0 ) } )
20	8 19 15	wbr	|- f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } )
21	13 20	wi	|- ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) )
22	21 3 7	wral	|- A. f e. ( II Cn j ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) )
23	22 1 2	crab	|- { j e. PConn | A. f e. ( II Cn j ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) }
24	0 23	wceq	|- SConn = { j e. PConn | A. f e. ( II Cn j ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` j ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) }