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 = { 𝑗 ∈ PConn ∣ ∀ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝑗 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csconn	⊢ SConn
1		vj	⊢ 𝑗
2		cpconn	⊢ PConn
3		vf	⊢ 𝑓
4		cii	⊢ II
5		ccn	⊢ Cn
6	1	cv	⊢ 𝑗
7	4 6 5	co	⊢ ( II Cn 𝑗 )
8	3	cv	⊢ 𝑓
9		cc0	⊢ 0
10	9 8	cfv	⊢ ( 𝑓 ‘ 0 )
11		c1	⊢ 1
12	11 8	cfv	⊢ ( 𝑓 ‘ 1 )
13	10 12	wceq	⊢ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 )
14		cphtpc	⊢ ≃ph
15	6 14	cfv	⊢ ( ≃ph ‘ 𝑗 )
16		cicc	⊢ [,]
17	9 11 16	co	⊢ ( 0 [,] 1 )
18	10	csn	⊢ { ( 𝑓 ‘ 0 ) }
19	17 18	cxp	⊢ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } )
20	8 19 15	wbr	⊢ 𝑓 ( ≃ph ‘ 𝑗 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } )
21	13 20	wi	⊢ ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝑗 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) )
22	21 3 7	wral	⊢ ∀ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝑗 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) )
23	22 1 2	crab	⊢ { 𝑗 ∈ PConn ∣ ∀ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝑗 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) }
24	0 23	wceq	⊢ SConn = { 𝑗 ∈ PConn ∣ ∀ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝑗 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) }