MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pi1 Structured version   Visualization version   GIF version

Definition df-pi1 24159
Description: Define the fundamental group, whose operation is given by concatenation of homotopy classes of loops. Definition of [Hatcher] p. 26. (Contributed by Mario Carneiro, 11-Feb-2015.)
Assertion
Ref Expression
df-pi1 π1 = (𝑗 ∈ Top, 𝑦 𝑗 ↦ ((𝑗 Ω1 𝑦) /s ( ≃ph𝑗)))
Distinct variable group:   𝑦,𝑗

Detailed syntax breakdown of Definition df-pi1
StepHypRef Expression
1 cpi1 24154 . 2 class π1
2 vj . . 3 setvar 𝑗
3 vy . . 3 setvar 𝑦
4 ctop 22030 . . 3 class Top
52cv 1538 . . . 4 class 𝑗
65cuni 4840 . . 3 class 𝑗
73cv 1538 . . . . 5 class 𝑦
8 comi 24152 . . . . 5 class Ω1
95, 7, 8co 7268 . . . 4 class (𝑗 Ω1 𝑦)
10 cphtpc 24120 . . . . 5 class ph
115, 10cfv 6427 . . . 4 class ( ≃ph𝑗)
12 cqus 17204 . . . 4 class /s
139, 11, 12co 7268 . . 3 class ((𝑗 Ω1 𝑦) /s ( ≃ph𝑗))
142, 3, 4, 6, 13cmpo 7270 . 2 class (𝑗 ∈ Top, 𝑦 𝑗 ↦ ((𝑗 Ω1 𝑦) /s ( ≃ph𝑗)))
151, 14wceq 1539 1 wff π1 = (𝑗 ∈ Top, 𝑦 𝑗 ↦ ((𝑗 Ω1 𝑦) /s ( ≃ph𝑗)))
Colors of variables: wff setvar class
This definition is referenced by:  pi1val  24188
  Copyright terms: Public domain W3C validator