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

Definition df-omn 19034
 Description: Define the n-th iterated loop space of a topological space. Unlike this is actually a pointed topological space, which is to say a tuple of a topological space (a member of , not ) and a point in the space. Higher loop spaces select the constant loop at the point from the lower loop space for the distinguished point. (Contributed by Mario Carneiro, 10-Jul-2015.)
Assertion
Ref Expression
df-omn TopSet
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-omn
StepHypRef Expression
1 comn 19029 . 2
2 vj . . 3
3 vy . . 3
4 ctop 16960 . . 3
52cv 1652 . . . 4
65cuni 4017 . . 3
7 vx . . . . . 6
8 vp . . . . . 6
9 cvv 2958 . . . . . 6
107cv 1652 . . . . . . . . . 10
11 c1st 6349 . . . . . . . . . 10
1210, 11cfv 5456 . . . . . . . . 9
13 ctopn 13651 . . . . . . . . 9
1412, 13cfv 5456 . . . . . . . 8
15 c2nd 6350 . . . . . . . . 9
1610, 15cfv 5456 . . . . . . . 8
17 comi 19028 . . . . . . . 8
1814, 16, 17co 6083 . . . . . . 7
19 cc0 8992 . . . . . . . . 9
20 c1 8993 . . . . . . . . 9
21 cicc 10921 . . . . . . . . 9
2219, 20, 21co 6083 . . . . . . . 8
2316csn 3816 . . . . . . . 8
2422, 23cxp 4878 . . . . . . 7
2518, 24cop 3819 . . . . . 6
267, 8, 9, 9, 25cmpt2 6085 . . . . 5
2726, 11ccom 4884 . . . 4
28 cnx 13468 . . . . . . . 8
29 cbs 13471 . . . . . . . 8
3028, 29cfv 5456 . . . . . . 7
3130, 6cop 3819 . . . . . 6
32 cts 13537 . . . . . . . 8 TopSet
3328, 32cfv 5456 . . . . . . 7 TopSet
3433, 5cop 3819 . . . . . 6 TopSet
3531, 34cpr 3817 . . . . 5 TopSet
363cv 1652 . . . . 5
3735, 36cop 3819 . . . 4 TopSet
3827, 37, 19cseq 11325 . . 3 TopSet
392, 3, 4, 6, 38cmpt2 6085 . 2 TopSet
401, 39wceq 1653 1 TopSet
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator