Database
BASIC TOPOLOGY
Metric spaces
The fundamental group
df-pi1
Metamath Proof Explorer
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 ‘ 𝑗 ) ) )