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

Definition df-omn 18521
Description: Define the n-th iterated loop space of a topological space. Unlike  Om 1 this is actually a pointed topological space, which is to say a tuple of a topological space (a member of  TopSp, not  Top) 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  |-  Om N  =  ( j  e. 
Top ,  y  e.  U. j  |->  seq  0 ( ( ( x  e. 
_V ,  p  e. 
_V  |->  <. ( ( TopOpen `  ( 1st `  x ) )  Om 1  ( 2nd `  x ) ) ,  ( ( 0 [,] 1 )  X.  { ( 2nd `  x ) } )
>. )  o.  1st ) ,  <. { <. (
Base `  ndx ) , 
U. j >. ,  <. (TopSet `  ndx ) ,  j
>. } ,  y >.
) )
Distinct variable group:    j, p, x, y

Detailed syntax breakdown of Definition df-omn
StepHypRef Expression
1 comn 18516 . 2  class  Om N
2 vj . . 3  set  j
3 vy . . 3  set  y
4 ctop 16647 . . 3  class  Top
52cv 1631 . . . 4  class  j
65cuni 3843 . . 3  class  U. j
7 vx . . . . . 6  set  x
8 vp . . . . . 6  set  p
9 cvv 2801 . . . . . 6  class  _V
107cv 1631 . . . . . . . . . 10  class  x
11 c1st 6136 . . . . . . . . . 10  class  1st
1210, 11cfv 5271 . . . . . . . . 9  class  ( 1st `  x )
13 ctopn 13342 . . . . . . . . 9  class  TopOpen
1412, 13cfv 5271 . . . . . . . 8  class  ( TopOpen `  ( 1st `  x ) )
15 c2nd 6137 . . . . . . . . 9  class  2nd
1610, 15cfv 5271 . . . . . . . 8  class  ( 2nd `  x )
17 comi 18515 . . . . . . . 8  class  Om 1
1814, 16, 17co 5874 . . . . . . 7  class  ( (
TopOpen `  ( 1st `  x
) )  Om 1 
( 2nd `  x
) )
19 cc0 8753 . . . . . . . . 9  class  0
20 c1 8754 . . . . . . . . 9  class  1
21 cicc 10675 . . . . . . . . 9  class  [,]
2219, 20, 21co 5874 . . . . . . . 8  class  ( 0 [,] 1 )
2316csn 3653 . . . . . . . 8  class  { ( 2nd `  x ) }
2422, 23cxp 4703 . . . . . . 7  class  ( ( 0 [,] 1 )  X.  { ( 2nd `  x ) } )
2518, 24cop 3656 . . . . . 6  class  <. (
( TopOpen `  ( 1st `  x ) )  Om 1  ( 2nd `  x
) ) ,  ( ( 0 [,] 1
)  X.  { ( 2nd `  x ) } ) >.
267, 8, 9, 9, 25cmpt2 5876 . . . . 5  class  ( x  e.  _V ,  p  e.  _V  |->  <. ( ( TopOpen `  ( 1st `  x ) )  Om 1  ( 2nd `  x ) ) ,  ( ( 0 [,] 1 )  X.  { ( 2nd `  x ) } )
>. )
2726, 11ccom 4709 . . . 4  class  ( ( x  e.  _V ,  p  e.  _V  |->  <. (
( TopOpen `  ( 1st `  x ) )  Om 1  ( 2nd `  x
) ) ,  ( ( 0 [,] 1
)  X.  { ( 2nd `  x ) } ) >. )  o.  1st )
28 cnx 13161 . . . . . . . 8  class  ndx
29 cbs 13164 . . . . . . . 8  class  Base
3028, 29cfv 5271 . . . . . . 7  class  ( Base `  ndx )
3130, 6cop 3656 . . . . . 6  class  <. ( Base `  ndx ) , 
U. j >.
32 cts 13230 . . . . . . . 8  class TopSet
3328, 32cfv 5271 . . . . . . 7  class  (TopSet `  ndx )
3433, 5cop 3656 . . . . . 6  class  <. (TopSet ` 
ndx ) ,  j
>.
3531, 34cpr 3654 . . . . 5  class  { <. (
Base `  ndx ) , 
U. j >. ,  <. (TopSet `  ndx ) ,  j
>. }
363cv 1631 . . . . 5  class  y
3735, 36cop 3656 . . . 4  class  <. { <. (
Base `  ndx ) , 
U. j >. ,  <. (TopSet `  ndx ) ,  j
>. } ,  y >.
3827, 37, 19cseq 11062 . . 3  class  seq  0
( ( ( x  e.  _V ,  p  e.  _V  |->  <. ( ( TopOpen `  ( 1st `  x ) )  Om 1  ( 2nd `  x ) ) ,  ( ( 0 [,] 1 )  X.  { ( 2nd `  x ) } )
>. )  o.  1st ) ,  <. { <. (
Base `  ndx ) , 
U. j >. ,  <. (TopSet `  ndx ) ,  j
>. } ,  y >.
)
392, 3, 4, 6, 38cmpt2 5876 . 2  class  ( j  e.  Top ,  y  e.  U. j  |->  seq  0 ( ( ( x  e.  _V ,  p  e.  _V  |->  <. (
( TopOpen `  ( 1st `  x ) )  Om 1  ( 2nd `  x
) ) ,  ( ( 0 [,] 1
)  X.  { ( 2nd `  x ) } ) >. )  o.  1st ) ,  <. {
<. ( Base `  ndx ) ,  U. j >. ,  <. (TopSet `  ndx ) ,  j >. } ,  y >. )
)
401, 39wceq 1632 1  wff  Om N  =  ( j  e. 
Top ,  y  e.  U. j  |->  seq  0 ( ( ( x  e. 
_V ,  p  e. 
_V  |->  <. ( ( TopOpen `  ( 1st `  x ) )  Om 1  ( 2nd `  x ) ) ,  ( ( 0 [,] 1 )  X.  { ( 2nd `  x ) } )
>. )  o.  1st ) ,  <. { <. (
Base `  ndx ) , 
U. j >. ,  <. (TopSet `  ndx ) ,  j
>. } ,  y >.
) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator