Definition df-sconn 32464

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 32462	. 2 class SConn
2		cc0 10531	. . . . . . 7 class 0
3		vf	. . . . . . . 8 setvar 𝑓
4	3	cv 1532	. . . . . . 7 class 𝑓
5	2, 4	cfv 6349	. . . . . 6 class (𝑓‘0)
6		c1 10532	. . . . . . 7 class 1
7	6, 4	cfv 6349	. . . . . 6 class (𝑓‘1)
8	5, 7	wceq 1533	. . . . 5 wff (𝑓‘0) = (𝑓‘1)
9		cicc 12735	. . . . . . . 8 class [,]
10	2, 6, 9	co 7150	. . . . . . 7 class (0[,]1)
11	5	csn 4560	. . . . . . 7 class {(𝑓‘0)}
12	10, 11	cxp 5547	. . . . . 6 class ((0[,]1) × {(𝑓‘0)})
13		vj	. . . . . . . 8 setvar 𝑗
14	13	cv 1532	. . . . . . 7 class 𝑗
15		cphtpc 23567	. . . . . . 7 class ≃ph
16	14, 15	cfv 6349	. . . . . 6 class ( ≃ph‘𝑗)
17	4, 12, 16	wbr 5058	. . . . 5 wff 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)})
18	8, 17	wi 4	. . . 4 wff ((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))
19		cii 23477	. . . . 5 class II
20		ccn 21826	. . . . 5 class Cn
21	19, 14, 20	co 7150	. . . 4 class (II Cn 𝑗)
22	18, 3, 21	wral 3138	. . 3 wff ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))
23		cpconn 32461	. . 3 class PConn
24	22, 13, 23	crab 3142	. 2 class {𝑗 ∈ PConn ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))}
25	1, 24	wceq 1533	1 wff SConn = {𝑗 ∈ PConn ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))}

This definition is referenced by:  issconn  32468