Definition df-pin 25042

Description: Define the n-th homotopy group, which is formed by taking the 𝑛-th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the 𝑛-th loop space, which is the 𝑛 − 1-th loop space. For 𝑛 = 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 𝑋. (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.)

Assertion

Ref	Expression
df-pin	⊢ πn = (𝑗 ∈ Top, 𝑝 ∈ ∪ 𝑗 ↦ (𝑛 ∈ ℕ0 ↦ ((1st ‘((𝑗 Ω𝑛 𝑝)‘𝑛)) /s if(𝑛 = 0, {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}, ( ≃ph‘(TopOpen‘(1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1)))))))))

Distinct variable group:   𝑓,𝑗,𝑛,𝑝,𝑥,𝑦

Detailed syntax breakdown of Definition df-pin

Step	Hyp	Ref	Expression
1		cpin 25037	. 2 class πn
2		vj	. . 3 setvar 𝑗
3		vp	. . 3 setvar 𝑝
4		ctop 22899	. . 3 class Top
5	2	cv 1539	. . . 4 class 𝑗
6	5	cuni 4907	. . 3 class ∪ 𝑗
7		vn	. . . 4 setvar 𝑛
8		cn0 12526	. . . 4 class ℕ0
9	7	cv 1539	. . . . . . 7 class 𝑛
10	3	cv 1539	. . . . . . . 8 class 𝑝
11		comn 25035	. . . . . . . 8 class Ω𝑛
12	5, 10, 11	co 7431	. . . . . . 7 class (𝑗 Ω𝑛 𝑝)
13	9, 12	cfv 6561	. . . . . 6 class ((𝑗 Ω𝑛 𝑝)‘𝑛)
14		c1st 8012	. . . . . 6 class 1st
15	13, 14	cfv 6561	. . . . 5 class (1st ‘((𝑗 Ω𝑛 𝑝)‘𝑛))
16		cc0 11155	. . . . . . 7 class 0
17	9, 16	wceq 1540	. . . . . 6 wff 𝑛 = 0
18		vf	. . . . . . . . . . . 12 setvar 𝑓
19	18	cv 1539	. . . . . . . . . . 11 class 𝑓
20	16, 19	cfv 6561	. . . . . . . . . 10 class (𝑓‘0)
21		vx	. . . . . . . . . . 11 setvar 𝑥
22	21	cv 1539	. . . . . . . . . 10 class 𝑥
23	20, 22	wceq 1540	. . . . . . . . 9 wff (𝑓‘0) = 𝑥
24		c1 11156	. . . . . . . . . . 11 class 1
25	24, 19	cfv 6561	. . . . . . . . . 10 class (𝑓‘1)
26		vy	. . . . . . . . . . 11 setvar 𝑦
27	26	cv 1539	. . . . . . . . . 10 class 𝑦
28	25, 27	wceq 1540	. . . . . . . . 9 wff (𝑓‘1) = 𝑦
29	23, 28	wa 395	. . . . . . . 8 wff ((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
30		cii 24901	. . . . . . . . 9 class II
31		ccn 23232	. . . . . . . . 9 class Cn
32	30, 5, 31	co 7431	. . . . . . . 8 class (II Cn 𝑗)
33	29, 18, 32	wrex 3070	. . . . . . 7 wff ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
34	33, 21, 26	copab 5205	. . . . . 6 class {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
35		cmin 11492	. . . . . . . . . . 11 class −
36	9, 24, 35	co 7431	. . . . . . . . . 10 class (𝑛 − 1)
37	36, 12	cfv 6561	. . . . . . . . 9 class ((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1))
38	37, 14	cfv 6561	. . . . . . . 8 class (1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1)))
39		ctopn 17466	. . . . . . . 8 class TopOpen
40	38, 39	cfv 6561	. . . . . . 7 class (TopOpen‘(1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1))))
41		cphtpc 25001	. . . . . . 7 class ≃ph
42	40, 41	cfv 6561	. . . . . 6 class ( ≃ph‘(TopOpen‘(1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1)))))
43	17, 34, 42	cif 4525	. . . . 5 class if(𝑛 = 0, {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}, ( ≃ph‘(TopOpen‘(1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1))))))
44		cqus 17550	. . . . 5 class /s
45	15, 43, 44	co 7431	. . . 4 class ((1st ‘((𝑗 Ω𝑛 𝑝)‘𝑛)) /s if(𝑛 = 0, {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}, ( ≃ph‘(TopOpen‘(1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1)))))))
46	7, 8, 45	cmpt 5225	. . 3 class (𝑛 ∈ ℕ0 ↦ ((1st ‘((𝑗 Ω𝑛 𝑝)‘𝑛)) /s if(𝑛 = 0, {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}, ( ≃ph‘(TopOpen‘(1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1))))))))
47	2, 3, 4, 6, 46	cmpo 7433	. 2 class (𝑗 ∈ Top, 𝑝 ∈ ∪ 𝑗 ↦ (𝑛 ∈ ℕ0 ↦ ((1st ‘((𝑗 Ω𝑛 𝑝)‘𝑛)) /s if(𝑛 = 0, {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}, ( ≃ph‘(TopOpen‘(1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1)))))))))
48	1, 47	wceq 1540	1 wff πn = (𝑗 ∈ Top, 𝑝 ∈ ∪ 𝑗 ↦ (𝑛 ∈ ℕ0 ↦ ((1st ‘((𝑗 Ω𝑛 𝑝)‘𝑛)) /s if(𝑛 = 0, {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}, ( ≃ph‘(TopOpen‘(1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1)))))))))

This definition is referenced by: (None)