Metamath Proof Explorer


Definition df-pi1

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)

Ref Expression
Assertion df-pi1 π1 = ( 𝑗 ∈ Top , 𝑦 𝑗 ↦ ( ( 𝑗 Ω1 𝑦 ) /s ( ≃ph𝑗 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpi1 π1
1 vj 𝑗
2 ctop Top
3 vy 𝑦
4 1 cv 𝑗
5 4 cuni 𝑗
6 comi Ω1
7 3 cv 𝑦
8 4 7 6 co ( 𝑗 Ω1 𝑦 )
9 cqus /s
10 cphtpc ph
11 4 10 cfv ( ≃ph𝑗 )
12 8 11 9 co ( ( 𝑗 Ω1 𝑦 ) /s ( ≃ph𝑗 ) )
13 1 3 2 5 12 cmpo ( 𝑗 ∈ Top , 𝑦 𝑗 ↦ ( ( 𝑗 Ω1 𝑦 ) /s ( ≃ph𝑗 ) ) )
14 0 13 wceq π1 = ( 𝑗 ∈ Top , 𝑦 𝑗 ↦ ( ( 𝑗 Ω1 𝑦 ) /s ( ≃ph𝑗 ) ) )