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	⊢ πn = ( 𝑗 ∈ Top , 𝑝 ∈ ∪ 𝑗 ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpin	⊢ πn
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vp	⊢ 𝑝
4	1	cv	⊢ 𝑗
5	4	cuni	⊢ ∪ 𝑗
6		vn	⊢ 𝑛
7		cn0	⊢ ℕ0
8		c1st	⊢ 1st
9		comn	⊢ Ω𝑛
10	3	cv	⊢ 𝑝
11	4 10 9	co	⊢ ( 𝑗 Ω𝑛 𝑝 )
12	6	cv	⊢ 𝑛
13	12 11	cfv	⊢ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 )
14	13 8	cfv	⊢ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) )
15		cqus	⊢ /s
16		cc0	⊢ 0
17	12 16	wceq	⊢ 𝑛 = 0
18		vx	⊢ 𝑥
19		vy	⊢ 𝑦
20		vf	⊢ 𝑓
21		cii	⊢ II
22		ccn	⊢ Cn
23	21 4 22	co	⊢ ( II Cn 𝑗 )
24	20	cv	⊢ 𝑓
25	16 24	cfv	⊢ ( 𝑓 ‘ 0 )
26	18	cv	⊢ 𝑥
27	25 26	wceq	⊢ ( 𝑓 ‘ 0 ) = 𝑥
28		c1	⊢ 1
29	28 24	cfv	⊢ ( 𝑓 ‘ 1 )
30	19	cv	⊢ 𝑦
31	29 30	wceq	⊢ ( 𝑓 ‘ 1 ) = 𝑦
32	27 31	wa	⊢ ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 )
33	32 20 23	wrex	⊢ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 )
34	33 18 19	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) }
35		cphtpc	⊢ ≃ph
36		ctopn	⊢ TopOpen
37		cmin	⊢ −
38	12 28 37	co	⊢ ( 𝑛 − 1 )
39	38 11	cfv	⊢ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) )
40	39 8	cfv	⊢ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) )
41	40 36	cfv	⊢ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) )
42	41 35	cfv	⊢ ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) )
43	17 34 42	cif	⊢ if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) )
44	14 43 15	co	⊢ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) )
45	6 7 44	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) )
46	1 3 2 5 45	cmpo	⊢ ( 𝑗 ∈ Top , 𝑝 ∈ ∪ 𝑗 ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) ) )
47	0 46	wceq	⊢ πn = ( 𝑗 ∈ Top , 𝑝 ∈ ∪ 𝑗 ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) ) )