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

Definition df-pi1 23604
 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 23599 . 2 class π1
2 vj . . 3 setvar 𝑗
3 vy . . 3 setvar 𝑦
4 ctop 21493 . . 3 class Top
52cv 1529 . . . 4 class 𝑗
65cuni 4830 . . 3 class 𝑗
73cv 1529 . . . . 5 class 𝑦
8 comi 23597 . . . . 5 class Ω1
95, 7, 8co 7148 . . . 4 class (𝑗 Ω1 𝑦)
10 cphtpc 23565 . . . . 5 class ph
115, 10cfv 6348 . . . 4 class ( ≃ph𝑗)
12 cqus 16770 . . . 4 class /s
139, 11, 12co 7148 . . 3 class ((𝑗 Ω1 𝑦) /s ( ≃ph𝑗))
142, 3, 4, 6, 13cmpo 7150 . 2 class (𝑗 ∈ Top, 𝑦 𝑗 ↦ ((𝑗 Ω1 𝑦) /s ( ≃ph𝑗)))
151, 14wceq 1530 1 wff π1 = (𝑗 ∈ Top, 𝑦 𝑗 ↦ ((𝑗 Ω1 𝑦) /s ( ≃ph𝑗)))
 Colors of variables: wff setvar class This definition is referenced by:  pi1val  23633
 Copyright terms: Public domain W3C validator