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	$$⊢{\pi }_1=\left(j\in \mathrm{Top},y\in \bigcup j⟼\left(j{\Omega }_{1}y\right){/}_{𝑠}{\simeq }_{\mathrm{ph}}\left(j\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpi1	$$class{\pi }_1$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vy	$$setvary$$
4	1	cv	$$setvarj$$
5	4	cuni	$$class\bigcup j$$
6		comi	$$class{\Omega }_1$$
7	3	cv	$$setvary$$
8	4 7 6	co	$$class\left(j{\Omega }_{1}y\right)$$
9		cqus	$$class{/}_{𝑠}$$
10		cphtpc	$$class{\simeq }_{\mathrm{ph}}$$
11	4 10	cfv	$$class{\simeq }_{\mathrm{ph}}\left(j\right)$$
12	8 11 9	co	$$class\left(\left(j{\Omega }_{1}y\right){/}_{𝑠}{\simeq }_{\mathrm{ph}}\left(j\right)\right)$$
13	1 3 2 5 12	cmpo	$$class\left(j\in \mathrm{Top},y\in \bigcup j⟼\left(j{\Omega }_{1}y\right){/}_{𝑠}{\simeq }_{\mathrm{ph}}\left(j\right)\right)$$
14	0 13	wceq	$$wff{\pi }_1=\left(j\in \mathrm{Top},y\in \bigcup j⟼\left(j{\Omega }_{1}y\right){/}_{𝑠}{\simeq }_{\mathrm{ph}}\left(j\right)\right)$$