Definition df-scon 30458

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.) (New usage is discouraged.)

Assertion

Ref	Expression
df-scon	⊢ SCon = {𝑗 ∈ PCon ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))}

Distinct variable group:   𝑓,𝑗

Detailed syntax breakdown of Definition df-scon

Step	Hyp	Ref	Expression
1		cscon 30456	. 2 class SCon
2		cc0 9815	. . . . . . 7 class 0
3		vf	. . . . . . . 8 setvar 𝑓
4	3	cv 1474	. . . . . . 7 class 𝑓
5	2, 4	cfv 5804	. . . . . 6 class (𝑓‘0)
6		c1 9816	. . . . . . 7 class 1
7	6, 4	cfv 5804	. . . . . 6 class (𝑓‘1)
8	5, 7	wceq 1475	. . . . 5 wff (𝑓‘0) = (𝑓‘1)
9		cicc 12049	. . . . . . . 8 class [,]
10	2, 6, 9	co 6549	. . . . . . 7 class (0[,]1)
11	5	csn 4125	. . . . . . 7 class {(𝑓‘0)}
12	10, 11	cxp 5036	. . . . . 6 class ((0[,]1) × {(𝑓‘0)})
13		vj	. . . . . . . 8 setvar 𝑗
14	13	cv 1474	. . . . . . 7 class 𝑗
15		cphtpc 22576	. . . . . . 7 class ≃ph
16	14, 15	cfv 5804	. . . . . 6 class ( ≃ph‘𝑗)
17	4, 12, 16	wbr 4583	. . . . 5 wff 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)})
18	8, 17	wi 4	. . . 4 wff ((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))
19		cii 22486	. . . . 5 class II
20		ccn 20838	. . . . 5 class Cn
21	19, 14, 20	co 6549	. . . 4 class (II Cn 𝑗)
22	18, 3, 21	wral 2896	. . 3 wff ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))
23		cpcon 30455	. . 3 class PCon
24	22, 13, 23	crab 2900	. 2 class {𝑗 ∈ PCon ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))}
25	1, 24	wceq 1475	1 wff SCon = {𝑗 ∈ PCon ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))}

This definition is referenced by:  isscon  30462