Definition df-omn 22807

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

Distinct variable group:   j, p, x, y

Detailed syntax breakdown of Definition df-omn

Step	Hyp	Ref	Expression
1		comn 22802	. 2 class OmN
2		vj	. . 3 setvar j
3		vy	. . 3 setvar y
4		ctop 20698	. . 3 class Top
5	2	cv 1482	. . . 4 class j
6	5	cuni 4436	. . 3 class U. j
7		vx	. . . . . 6 setvar x
8		vp	. . . . . 6 setvar p
9		cvv 3200	. . . . . 6 class _V
10	7	cv 1482	. . . . . . . . . 10 class x
11		c1st 7166	. . . . . . . . . 10 class 1st
12	10, 11	cfv 5888	. . . . . . . . 9 class ( 1st ` x )
13		ctopn 16082	. . . . . . . . 9 class TopOpen
14	12, 13	cfv 5888	. . . . . . . 8 class ( TopOpen ` ( 1st ` x ) )
15		c2nd 7167	. . . . . . . . 9 class 2nd
16	10, 15	cfv 5888	. . . . . . . 8 class ( 2nd ` x )
17		comi 22801	. . . . . . . 8 class Om1
18	14, 16, 17	co 6650	. . . . . . 7 class ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) )
19		cc0 9936	. . . . . . . . 9 class 0
20		c1 9937	. . . . . . . . 9 class 1
21		cicc 12178	. . . . . . . . 9 class [,]
22	19, 20, 21	co 6650	. . . . . . . 8 class ( 0 [,] 1 )
23	16	csn 4177	. . . . . . . 8 class { ( 2nd ` x ) }
24	22, 23	cxp 5112	. . . . . . 7 class ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } )
25	18, 24	cop 4183	. . . . . 6 class <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >.
26	7, 8, 9, 9, 25	cmpt2 6652	. . . . 5 class ( x e. _V , p e. _V |-> <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >. )
27	26, 11	ccom 5118	. . . 4 class ( ( x e. _V , p e. _V |-> <. ( ( TopOpen ` ( 1st ` x ) ) Om1 ( 2nd ` x ) ) , ( ( 0 [,] 1 ) X. { ( 2nd ` x ) } ) >. ) o. 1st )
28		cnx 15854	. . . . . . . 8 class ndx
29		cbs 15857	. . . . . . . 8 class Base
30	28, 29	cfv 5888	. . . . . . 7 class ( Base ` ndx )
31	30, 6	cop 4183	. . . . . 6 class <. ( Base ` ndx ) , U. j >.
32		cts 15947	. . . . . . . 8 class TopSet
33	28, 32	cfv 5888	. . . . . . 7 class (TopSet ` ndx )
34	33, 5	cop 4183	. . . . . 6 class <. (TopSet ` ndx ) , j >.
35	31, 34	cpr 4179	. . . . 5 class { <. ( Base ` ndx ) , U. j >. , <. (TopSet ` ndx ) , j >. }
36	3	cv 1482	. . . . 5 class y
37	35, 36	cop 4183	. . . 4 class <. { <. ( Base ` ndx ) , U. j >. , <. (TopSet ` ndx ) , j >. } , y >.
38	27, 37, 19	cseq 12801	. . 3 class 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	2, 3, 4, 6, 38	cmpt2 6652	. 2 class ( 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 >. ) )
40	1, 39	wceq 1483	1 wff 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 >. ) )

This definition is referenced by: (None)