Definition df-sconn 35227

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

Distinct variable group:   𝑓,𝑗

Detailed syntax breakdown of Definition df-sconn

Step	Hyp	Ref	Expression
1		csconn 35225	. 2 class SConn
2		cc0 11155	. . . . . . 7 class 0
3		vf	. . . . . . . 8 setvar 𝑓
4	3	cv 1539	. . . . . . 7 class 𝑓
5	2, 4	cfv 6561	. . . . . 6 class (𝑓‘0)
6		c1 11156	. . . . . . 7 class 1
7	6, 4	cfv 6561	. . . . . 6 class (𝑓‘1)
8	5, 7	wceq 1540	. . . . 5 wff (𝑓‘0) = (𝑓‘1)
9		cicc 13390	. . . . . . . 8 class [,]
10	2, 6, 9	co 7431	. . . . . . 7 class (0[,]1)
11	5	csn 4626	. . . . . . 7 class {(𝑓‘0)}
12	10, 11	cxp 5683	. . . . . 6 class ((0[,]1) × {(𝑓‘0)})
13		vj	. . . . . . . 8 setvar 𝑗
14	13	cv 1539	. . . . . . 7 class 𝑗
15		cphtpc 25001	. . . . . . 7 class ≃ph
16	14, 15	cfv 6561	. . . . . 6 class ( ≃ph‘𝑗)
17	4, 12, 16	wbr 5143	. . . . 5 wff 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)})
18	8, 17	wi 4	. . . 4 wff ((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))
19		cii 24901	. . . . 5 class II
20		ccn 23232	. . . . 5 class Cn
21	19, 14, 20	co 7431	. . . 4 class (II Cn 𝑗)
22	18, 3, 21	wral 3061	. . 3 wff ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))
23		cpconn 35224	. . 3 class PConn
24	22, 13, 23	crab 3436	. 2 class {𝑗 ∈ PConn ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))}
25	1, 24	wceq 1540	1 wff SConn = {𝑗 ∈ PConn ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))}

This definition is referenced by:  issconn  35231