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

Definition df-om1 21269
 Description: Define the loop space of a topological space, with a magma structure on it given by concatenation of loops. This structure is not a group, but the operation is compatible with homotopy, which allows the homotopy groups to be defined based on this operation. (Contributed by Mario Carneiro, 10-Jul-2015.)
Assertion
Ref Expression
df-om1 TopSet
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-om1
StepHypRef Expression
1 comi 21264 . 2
2 vj . . 3
3 vy . . 3
4 ctop 19189 . . 3
52cv 1378 . . . 4
65cuni 4245 . . 3
7 cnx 14487 . . . . . 6
8 cbs 14490 . . . . . 6
97, 8cfv 5588 . . . . 5
10 cc0 9492 . . . . . . . . 9
11 vf . . . . . . . . . 10
1211cv 1378 . . . . . . . . 9
1310, 12cfv 5588 . . . . . . . 8
143cv 1378 . . . . . . . 8
1513, 14wceq 1379 . . . . . . 7
16 c1 9493 . . . . . . . . 9
1716, 12cfv 5588 . . . . . . . 8
1817, 14wceq 1379 . . . . . . 7
1915, 18wa 369 . . . . . 6
20 cii 21142 . . . . . . 7
21 ccn 19519 . . . . . . 7
2220, 5, 21co 6284 . . . . . 6
2319, 11, 22crab 2818 . . . . 5
249, 23cop 4033 . . . 4
25 cplusg 14555 . . . . . 6
267, 25cfv 5588 . . . . 5
27 cpco 21263 . . . . . 6
285, 27cfv 5588 . . . . 5
2926, 28cop 4033 . . . 4
30 cts 14561 . . . . . 6 TopSet
317, 30cfv 5588 . . . . 5 TopSet
32 cxko 19825 . . . . . 6
335, 20, 32co 6284 . . . . 5
3431, 33cop 4033 . . . 4 TopSet
3524, 29, 34ctp 4031 . . 3 TopSet
362, 3, 4, 6, 35cmpt2 6286 . 2 TopSet
371, 36wceq 1379 1 TopSet
 Colors of variables: wff setvar class This definition is referenced by:  om1val  21293
 Copyright terms: Public domain W3C validator