Metamath Proof Explorer

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 ⊢ π 𝑛 = j ∈ Top , p ∈ ⋃ j ⟼ n ∈ ℕ 0 ⟼ 1 st ⁡ j Ω 𝑛 p ⁡ n / 𝑠 if n = 0 x y | ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y ≃ ph ⁡ TopOpen ⁡ 1 st ⁡ j Ω 𝑛 p ⁡ n − 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpin class π 𝑛
1 vj setvar j
2 ctop class Top
3 vp setvar p
4 1 cv setvar j
5 4 cuni class ⋃ j
6 vn setvar n
7 cn0 class ℕ 0
8 c1st class 1 st
9 comn class Ω 𝑛
10 3 cv setvar p
11 4 10 9 co class j Ω 𝑛 p
12 6 cv setvar n
13 12 11 cfv class j Ω 𝑛 p ⁡ n
14 13 8 cfv class 1 st ⁡ j Ω 𝑛 p ⁡ n
15 cqus class / 𝑠
16 cc0 class 0
17 12 16 wceq wff n = 0
18 vx setvar x
19 vy setvar y
20 vf setvar f
21 cii class II
22 ccn class Cn
23 21 4 22 co class II Cn j
24 20 cv setvar f
25 16 24 cfv class f ⁡ 0
26 18 cv setvar x
27 25 26 wceq wff f ⁡ 0 = x
28 c1 class 1
29 28 24 cfv class f ⁡ 1
30 19 cv setvar y
31 29 30 wceq wff f ⁡ 1 = y
32 27 31 wa wff f ⁡ 0 = x ∧ f ⁡ 1 = y
33 32 20 23 wrex wff ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y
34 33 18 19 copab class x y | ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y
35 cphtpc class ≃ ph
36 ctopn class TopOpen
37 cmin class −
38 12 28 37 co class n − 1
39 38 11 cfv class j Ω 𝑛 p ⁡ n − 1
40 39 8 cfv class 1 st ⁡ j Ω 𝑛 p ⁡ n − 1
41 40 36 cfv class TopOpen ⁡ 1 st ⁡ j Ω 𝑛 p ⁡ n − 1
42 41 35 cfv class ≃ ph ⁡ TopOpen ⁡ 1 st ⁡ j Ω 𝑛 p ⁡ n − 1
43 17 34 42 cif class if n = 0 x y | ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y ≃ ph ⁡ TopOpen ⁡ 1 st ⁡ j Ω 𝑛 p ⁡ n − 1
44 14 43 15 co class 1 st ⁡ j Ω 𝑛 p ⁡ n / 𝑠 if n = 0 x y | ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y ≃ ph ⁡ TopOpen ⁡ 1 st ⁡ j Ω 𝑛 p ⁡ n − 1
45 6 7 44 cmpt class n ∈ ℕ 0 ⟼ 1 st ⁡ j Ω 𝑛 p ⁡ n / 𝑠 if n = 0 x y | ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y ≃ ph ⁡ TopOpen ⁡ 1 st ⁡ j Ω 𝑛 p ⁡ n − 1
46 1 3 2 5 45 cmpo class j ∈ Top , p ∈ ⋃ j ⟼ n ∈ ℕ 0 ⟼ 1 st ⁡ j Ω 𝑛 p ⁡ n / 𝑠 if n = 0 x y | ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y ≃ ph ⁡ TopOpen ⁡ 1 st ⁡ j Ω 𝑛 p ⁡ n − 1
47 0 46 wceq wff π 𝑛 = j ∈ Top , p ∈ ⋃ j ⟼ n ∈ ℕ 0 ⟼ 1 st ⁡ j Ω 𝑛 p ⁡ n / 𝑠 if n = 0 x y | ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y ≃ ph ⁡ TopOpen ⁡ 1 st ⁡ j Ω 𝑛 p ⁡ n − 1