Definition df-pin

Description: Define the n-th homotopy group, which is formed by taking the n -th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the n -th loop space, which is the n - 1 -th loop space. For n = 0 , since this is not well-defined we replace this relation with the path-connectedness relation, so that the 0 -th homotopy group is the set of path components of X . (Since the 0 -th loop space does not have a group operation, neither does the 0 -th homotopy group, but the rest are genuine groups.) (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	df-pin	$$⊢{\pi }_{\mathrm{𝑛}}=\left(j\in \mathrm{Top},p\in \bigcup j⟼\left(n\in {\mathbb{N}}_0⟼1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n\right)\right){/}_{𝑠}if\left(n=0,\left\{⟨x,y⟩|\exists f\in \left(\mathrm{II}\mathrm{Cn}j\right)\left(f\left(0\right)=x\wedge f\left(1\right)=y\right)\right\},{\simeq }_{\mathrm{ph}}\left(\mathrm{TopOpen}\left(1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n-1\right)\right)\right)\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpin	$$class{\pi }_{\mathrm{𝑛}}$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vp	$$setvarp$$
4	1	cv	$$setvarj$$
5	4	cuni	$$class\bigcup j$$
6		vn	$$setvarn$$
7		cn0	$$class{\mathbb{N}}_0$$
8		c1st	$$class{1}^{st}$$
9		comn	$$class{\Omega }_{\mathrm{𝑛}}$$
10	3	cv	$$setvarp$$
11	4 10 9	co	$$class\left(j{\Omega }_{\mathrm{𝑛}}p\right)$$
12	6	cv	$$setvarn$$
13	12 11	cfv	$$class\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n\right)$$
14	13 8	cfv	$$class{1}^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n\right)\right)$$
15		cqus	$$class{/}_{𝑠}$$
16		cc0	$$class0$$
17	12 16	wceq	$$wffn=0$$
18		vx	$$setvarx$$
19		vy	$$setvary$$
20		vf	$$setvarf$$
21		cii	$$class\mathrm{II}$$
22		ccn	$$class\mathrm{Cn}$$
23	21 4 22	co	$$class\left(\mathrm{II}\mathrm{Cn}j\right)$$
24	20	cv	$$setvarf$$
25	16 24	cfv	$$classf\left(0\right)$$
26	18	cv	$$setvarx$$
27	25 26	wceq	$$wfff\left(0\right)=x$$
28		c1	$$class1$$
29	28 24	cfv	$$classf\left(1\right)$$
30	19	cv	$$setvary$$
31	29 30	wceq	$$wfff\left(1\right)=y$$
32	27 31	wa	$$wff\left(f\left(0\right)=x\wedge f\left(1\right)=y\right)$$
33	32 20 23	wrex	$$wff\exists f\in \left(\mathrm{II}\mathrm{Cn}j\right)\left(f\left(0\right)=x\wedge f\left(1\right)=y\right)$$
34	33 18 19	copab	$$class\left\{⟨x,y⟩|\exists f\in \left(\mathrm{II}\mathrm{Cn}j\right)\left(f\left(0\right)=x\wedge f\left(1\right)=y\right)\right\}$$
35		cphtpc	$$class{\simeq }_{\mathrm{ph}}$$
36		ctopn	$$class\mathrm{TopOpen}$$
37		cmin	$$class-$$
38	12 28 37	co	$$class\left(n-1\right)$$
39	38 11	cfv	$$class\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n-1\right)$$
40	39 8	cfv	$$class{1}^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n-1\right)\right)$$
41	40 36	cfv	$$class\mathrm{TopOpen}\left(1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n-1\right)\right)\right)$$
42	41 35	cfv	$$class{\simeq }_{\mathrm{ph}}\left(\mathrm{TopOpen}\left(1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n-1\right)\right)\right)\right)$$
43	17 34 42	cif	$$classif\left(n=0,\left\{⟨x,y⟩|\exists f\in \left(\mathrm{II}\mathrm{Cn}j\right)\left(f\left(0\right)=x\wedge f\left(1\right)=y\right)\right\},{\simeq }_{\mathrm{ph}}\left(\mathrm{TopOpen}\left(1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n-1\right)\right)\right)\right)\right)$$
44	14 43 15	co	$$class\left(1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n\right)\right){/}_{𝑠}if\left(n=0,\left\{⟨x,y⟩|\exists f\in \left(\mathrm{II}\mathrm{Cn}j\right)\left(f\left(0\right)=x\wedge f\left(1\right)=y\right)\right\},{\simeq }_{\mathrm{ph}}\left(\mathrm{TopOpen}\left(1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n-1\right)\right)\right)\right)\right)\right)$$
45	6 7 44	cmpt	$$class\left(n\in {\mathbb{N}}_0⟼1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n\right)\right){/}_{𝑠}if\left(n=0,\left\{⟨x,y⟩|\exists f\in \left(\mathrm{II}\mathrm{Cn}j\right)\left(f\left(0\right)=x\wedge f\left(1\right)=y\right)\right\},{\simeq }_{\mathrm{ph}}\left(\mathrm{TopOpen}\left(1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n-1\right)\right)\right)\right)\right)\right)$$
46	1 3 2 5 45	cmpo	$$class\left(j\in \mathrm{Top},p\in \bigcup j⟼\left(n\in {\mathbb{N}}_0⟼1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n\right)\right){/}_{𝑠}if\left(n=0,\left\{⟨x,y⟩|\exists f\in \left(\mathrm{II}\mathrm{Cn}j\right)\left(f\left(0\right)=x\wedge f\left(1\right)=y\right)\right\},{\simeq }_{\mathrm{ph}}\left(\mathrm{TopOpen}\left(1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n-1\right)\right)\right)\right)\right)\right)\right)$$
47	0 46	wceq	$$wff{\pi }_{\mathrm{𝑛}}=\left(j\in \mathrm{Top},p\in \bigcup j⟼\left(n\in {\mathbb{N}}_0⟼1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n\right)\right){/}_{𝑠}if\left(n=0,\left\{⟨x,y⟩|\exists f\in \left(\mathrm{II}\mathrm{Cn}j\right)\left(f\left(0\right)=x\wedge f\left(1\right)=y\right)\right\},{\simeq }_{\mathrm{ph}}\left(\mathrm{TopOpen}\left(1^{st}\left(\left(j{\Omega }_{\mathrm{𝑛}}p\right)\left(n-1\right)\right)\right)\right)\right)\right)\right)$$