Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pin Structured version   Unicode version

Definition df-pin 19034
 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 -th loop space. For , since this is not well-defined we replace this relation with the path-connectedness relation, so that the -th homotopy group is the set of path components of . (Since the -th loop space does not have a group operation, neither does the -th homotopy group, but the rest are genuine groups.) (Contributed by Mario Carneiro, 11-Feb-2015.)
Assertion
Ref Expression
df-pin s
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-pin
StepHypRef Expression
1 cpin 19029 . 2
2 vj . . 3
3 vp . . 3
4 ctop 16958 . . 3
52cv 1651 . . . 4
65cuni 4015 . . 3
7 vn . . . 4
8 cn0 10221 . . . 4
97cv 1651 . . . . . . 7
103cv 1651 . . . . . . . 8
11 comn 19027 . . . . . . . 8
125, 10, 11co 6081 . . . . . . 7
139, 12cfv 5454 . . . . . 6
14 c1st 6347 . . . . . 6
1513, 14cfv 5454 . . . . 5
16 cc0 8990 . . . . . . 7
179, 16wceq 1652 . . . . . 6
18 vf . . . . . . . . . . . 12
1918cv 1651 . . . . . . . . . . 11
2016, 19cfv 5454 . . . . . . . . . 10
21 vx . . . . . . . . . . 11
2221cv 1651 . . . . . . . . . 10
2320, 22wceq 1652 . . . . . . . . 9
24 c1 8991 . . . . . . . . . . 11
2524, 19cfv 5454 . . . . . . . . . 10
26 vy . . . . . . . . . . 11
2726cv 1651 . . . . . . . . . 10
2825, 27wceq 1652 . . . . . . . . 9
2923, 28wa 359 . . . . . . . 8
30 cii 18905 . . . . . . . . 9
31 ccn 17288 . . . . . . . . 9
3230, 5, 31co 6081 . . . . . . . 8
3329, 18, 32wrex 2706 . . . . . . 7
3433, 21, 26copab 4265 . . . . . 6
35 cmin 9291 . . . . . . . . . . 11
369, 24, 35co 6081 . . . . . . . . . 10
3736, 12cfv 5454 . . . . . . . . 9
3837, 14cfv 5454 . . . . . . . 8
39 ctopn 13649 . . . . . . . 8
4038, 39cfv 5454 . . . . . . 7
41 cphtpc 18994 . . . . . . 7
4240, 41cfv 5454 . . . . . 6
4317, 34, 42cif 3739 . . . . 5
44 cqus 13731 . . . . 5 s
4515, 43, 44co 6081 . . . 4 s
467, 8, 45cmpt 4266 . . 3 s
472, 3, 4, 6, 46cmpt2 6083 . 2 s
481, 47wceq 1652 1 s
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator