Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sconn Structured version   Visualization version   GIF version

Definition df-sconn 30965
 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
StepHypRef Expression
1 csconn 30963 . 2 class SConn
2 cc0 9896 . . . . . . 7 class 0
3 vf . . . . . . . 8 setvar 𝑓
43cv 1479 . . . . . . 7 class 𝑓
52, 4cfv 5857 . . . . . 6 class (𝑓‘0)
6 c1 9897 . . . . . . 7 class 1
76, 4cfv 5857 . . . . . 6 class (𝑓‘1)
85, 7wceq 1480 . . . . 5 wff (𝑓‘0) = (𝑓‘1)
9 cicc 12136 . . . . . . . 8 class [,]
102, 6, 9co 6615 . . . . . . 7 class (0[,]1)
115csn 4155 . . . . . . 7 class {(𝑓‘0)}
1210, 11cxp 5082 . . . . . 6 class ((0[,]1) × {(𝑓‘0)})
13 vj . . . . . . . 8 setvar 𝑗
1413cv 1479 . . . . . . 7 class 𝑗
15 cphtpc 22708 . . . . . . 7 class ph
1614, 15cfv 5857 . . . . . 6 class ( ≃ph𝑗)
174, 12, 16wbr 4623 . . . . 5 wff 𝑓( ≃ph𝑗)((0[,]1) × {(𝑓‘0)})
188, 17wi 4 . . . 4 wff ((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph𝑗)((0[,]1) × {(𝑓‘0)}))
19 cii 22618 . . . . 5 class II
20 ccn 20968 . . . . 5 class Cn
2119, 14, 20co 6615 . . . 4 class (II Cn 𝑗)
2218, 3, 21wral 2908 . . 3 wff 𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph𝑗)((0[,]1) × {(𝑓‘0)}))
23 cpconn 30962 . . 3 class PConn
2422, 13, 23crab 2912 . 2 class {𝑗 ∈ PConn ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph𝑗)((0[,]1) × {(𝑓‘0)}))}
251, 24wceq 1480 1 wff SConn = {𝑗 ∈ PConn ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph𝑗)((0[,]1) × {(𝑓‘0)}))}
 Colors of variables: wff setvar class This definition is referenced by:  issconn  30969
 Copyright terms: Public domain W3C validator