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

Definition df-om1 19031
 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 19026 . 2
2 vj . . 3
3 vy . . 3
4 ctop 16958 . . 3
52cv 1651 . . . 4
65cuni 4015 . . 3
7 cnx 13466 . . . . . 6
8 cbs 13469 . . . . . 6
97, 8cfv 5454 . . . . 5
10 cc0 8990 . . . . . . . . 9
11 vf . . . . . . . . . 10
1211cv 1651 . . . . . . . . 9
1310, 12cfv 5454 . . . . . . . 8
143cv 1651 . . . . . . . 8
1513, 14wceq 1652 . . . . . . 7
16 c1 8991 . . . . . . . . 9
1716, 12cfv 5454 . . . . . . . 8
1817, 14wceq 1652 . . . . . . 7
1915, 18wa 359 . . . . . 6
20 cii 18905 . . . . . . 7
21 ccn 17288 . . . . . . 7
2220, 5, 21co 6081 . . . . . 6
2319, 11, 22crab 2709 . . . . 5
249, 23cop 3817 . . . 4
25 cplusg 13529 . . . . . 6
267, 25cfv 5454 . . . . 5
27 cpco 19025 . . . . . 6
285, 27cfv 5454 . . . . 5
2926, 28cop 3817 . . . 4
30 cts 13535 . . . . . 6 TopSet
317, 30cfv 5454 . . . . 5 TopSet
32 cxko 17593 . . . . . 6
335, 20, 32co 6081 . . . . 5
3431, 33cop 3817 . . . 4 TopSet
3524, 29, 34ctp 3816 . . 3 TopSet
362, 3, 4, 6, 35cmpt2 6083 . 2 TopSet
371, 36wceq 1652 1 TopSet
 Colors of variables: wff set class This definition is referenced by:  om1val  19055
 Copyright terms: Public domain W3C validator