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	⊢ Ω𝑛 = ( 𝑗 ∈ Top , 𝑦 ∈ ∪ 𝑗 ↦ seq 0 ( ( ( 𝑥 ∈ V , 𝑝 ∈ V ↦ ⟨ ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) ⟩ ) ∘ 1st ) , ⟨ { ⟨ ( Base ‘ ndx ) , ∪ 𝑗 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝑗 ⟩ } , 𝑦 ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		comn	⊢ Ω𝑛
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑗
5	4	cuni	⊢ ∪ 𝑗
6		cc0	⊢ 0
7		vx	⊢ 𝑥
8		cvv	⊢ V
9		vp	⊢ 𝑝
10		ctopn	⊢ TopOpen
11		c1st	⊢ 1st
12	7	cv	⊢ 𝑥
13	12 11	cfv	⊢ ( 1st ‘ 𝑥 )
14	13 10	cfv	⊢ ( TopOpen ‘ ( 1st ‘ 𝑥 ) )
15		comi	⊢ Ω1
16		c2nd	⊢ 2nd
17	12 16	cfv	⊢ ( 2nd ‘ 𝑥 )
18	14 17 15	co	⊢ ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) )
19		cicc	⊢ [,]
20		c1	⊢ 1
21	6 20 19	co	⊢ ( 0 [,] 1 )
22	17	csn	⊢ { ( 2nd ‘ 𝑥 ) }
23	21 22	cxp	⊢ ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } )
24	18 23	cop	⊢ ⟨ ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) ⟩
25	7 9 8 8 24	cmpo	⊢ ( 𝑥 ∈ V , 𝑝 ∈ V ↦ ⟨ ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) ⟩ )
26	25 11	ccom	⊢ ( ( 𝑥 ∈ V , 𝑝 ∈ V ↦ ⟨ ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) ⟩ ) ∘ 1st )
27		cbs	⊢ Base
28		cnx	⊢ ndx
29	28 27	cfv	⊢ ( Base ‘ ndx )
30	29 5	cop	⊢ ⟨ ( Base ‘ ndx ) , ∪ 𝑗 ⟩
31		cts	⊢ TopSet
32	28 31	cfv	⊢ ( TopSet ‘ ndx )
33	32 4	cop	⊢ ⟨ ( TopSet ‘ ndx ) , 𝑗 ⟩
34	30 33	cpr	⊢ { ⟨ ( Base ‘ ndx ) , ∪ 𝑗 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝑗 ⟩ }
35	3	cv	⊢ 𝑦
36	34 35	cop	⊢ ⟨ { ⟨ ( Base ‘ ndx ) , ∪ 𝑗 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝑗 ⟩ } , 𝑦 ⟩
37	26 36 6	cseq	⊢ seq 0 ( ( ( 𝑥 ∈ V , 𝑝 ∈ V ↦ ⟨ ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) ⟩ ) ∘ 1st ) , ⟨ { ⟨ ( Base ‘ ndx ) , ∪ 𝑗 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝑗 ⟩ } , 𝑦 ⟩ )
38	1 3 2 5 37	cmpo	⊢ ( 𝑗 ∈ Top , 𝑦 ∈ ∪ 𝑗 ↦ seq 0 ( ( ( 𝑥 ∈ V , 𝑝 ∈ V ↦ ⟨ ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) ⟩ ) ∘ 1st ) , ⟨ { ⟨ ( Base ‘ ndx ) , ∪ 𝑗 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝑗 ⟩ } , 𝑦 ⟩ ) )
39	0 38	wceq	⊢ Ω𝑛 = ( 𝑗 ∈ Top , 𝑦 ∈ ∪ 𝑗 ↦ seq 0 ( ( ( 𝑥 ∈ V , 𝑝 ∈ V ↦ ⟨ ( ( TopOpen ‘ ( 1st ‘ 𝑥 ) ) Ω1 ( 2nd ‘ 𝑥 ) ) , ( ( 0 [,] 1 ) × { ( 2nd ‘ 𝑥 ) } ) ⟩ ) ∘ 1st ) , ⟨ { ⟨ ( Base ‘ ndx ) , ∪ 𝑗 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝑗 ⟩ } , 𝑦 ⟩ ) )