Metamath Proof Explorer

Definition df-omn

Description: Define the n-th iterated loop space of a topological space. Unlike Om1 this is actually apointed 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)

Ref Expression
Assertion df-omn 
|- OmN = ( j e. Top , y e. U. j |-> seq 0 ( ( ( x e. _V , p e. _V |-> <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >. ) o. 1st ) , <. { <. ( Base ` ndx ) , U. j >. , <. ( TopSet ` ndx ) , j >. } , y >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 comn 
 |-  OmN
1 vj 
 |-  j
2 ctop 
 |-  Top
3 vy 
 |-  y
4 1 cv 
 |-  j
5 4 cuni 
 |-  U. j
6 cc0 
 |-  0
7 vx 
 |-  x
8 cvv 
 |-  _V
9 vp 
 |-  p
10 ctopn 
 |-  TopOpen
11 c1st 
 |-  1st
12 7 cv 
 |-  x
13 12 11 cfv 
 |-  ( 1st ` x )
14 13 10 cfv 
 |-  ( TopOpen ` ( 1st ` x ) )
15 comi 
 |-  Om1
16 c2nd 
 |-  2nd
17 12 16 cfv 
 |-  ( 2nd ` x )
18 14 17 15 co 
 |-  ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) )
19 cicc 
 |-  [,]
20 c1 
 |-  1
21 6 20 19 co 
 |-  ( 0 [,] 1 )
22 17 csn 
 |-  { ( 2nd ` x ) }
23 21 22 cxp 
 |-  ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } )
24 18 23 cop 
 |-  <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >.
25 7 9 8 8 24 cmpo 
 |-  ( x e. _V , p e. _V |-> <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >. )
26 25 11 ccom 
 |-  ( ( x e. _V , p e. _V |-> <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >. ) o. 1st )
27 cbs 
 |-  Base
28 cnx 
 |-  ndx
29 28 27 cfv 
 |-  ( Base ` ndx )
30 29 5 cop 
 |-  <. ( Base ` ndx ) , U. j >.
31 cts 
 |-  TopSet
32 28 31 cfv 
 |-  ( TopSet ` ndx )
33 32 4 cop 
 |-  <. ( TopSet ` ndx ) , j >.
34 30 33 cpr 
 |-  { <. ( Base ` ndx ) , U. j >. , <. ( TopSet ` ndx ) , j >. }
35 3 cv 
 |-  y
36 34 35 cop 
 |-  <. { <. ( Base ` ndx ) , U. j >. , <. ( TopSet ` ndx ) , j >. } , y >.
37 26 36 6 cseq 
 |-  seq 0 ( ( ( x e. _V , p e. _V |-> <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >. ) o. 1st ) , <. { <. ( Base ` ndx ) , U. j >. , <. ( TopSet ` ndx ) , j >. } , y >. )
38 1 3 2 5 37 cmpo 
 |-  ( j e. Top , y e. U. j |-> seq 0 ( ( ( x e. _V , p e. _V |-> <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >. ) o. 1st ) , <. { <. ( Base ` ndx ) , U. j >. , <. ( TopSet ` ndx ) , j >. } , y >. ) )
39 0 38 wceq 
 |-  OmN = ( j e. Top , y e. U. j |-> seq 0 ( ( ( x e. _V , p e. _V |-> <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >. ) o. 1st ) , <. { <. ( Base ` ndx ) , U. j >. , <. ( TopSet ` ndx ) , j >. } , y >. ) )