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 ‘ 𝑗 ) ) )