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 22789
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 22784 . 2 class π1
2 vj . . 3 setvar 𝑗
3 vy . . 3 setvar 𝑦
4 ctop 20679 . . 3 class Top
52cv 1480 . . . 4 class 𝑗
65cuni 4427 . . 3 class 𝑗
73cv 1480 . . . . 5 class 𝑦
8 comi 22782 . . . . 5 class Ω1
95, 7, 8co 6635 . . . 4 class (𝑗 Ω1 𝑦)
10 cphtpc 22749 . . . . 5 class ph
115, 10cfv 5876 . . . 4 class ( ≃ph𝑗)
12 cqus 16146 . . . 4 class /s
139, 11, 12co 6635 . . 3 class ((𝑗 Ω1 𝑦) /s ( ≃ph𝑗))
142, 3, 4, 6, 13cmpt2 6637 . 2 class (𝑗 ∈ Top, 𝑦 𝑗 ↦ ((𝑗 Ω1 𝑦) /s ( ≃ph𝑗)))
151, 14wceq 1481 1 wff π1 = (𝑗 ∈ Top, 𝑦 𝑗 ↦ ((𝑗 Ω1 𝑦) /s ( ≃ph𝑗)))
Colors of variables: wff setvar class
This definition is referenced by:  pi1val  22818
  Copyright terms: Public domain W3C validator