Definition df-omn 23605

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

Distinct variable group:   𝑗,𝑝,𝑥,𝑦

Detailed syntax breakdown of Definition df-omn

Step	Hyp	Ref	Expression
1		comn 23600	. 2 class Ω𝑛
2		vj	. . 3 setvar 𝑗
3		vy	. . 3 setvar 𝑦
4		ctop 21495	. . 3 class Top
5	2	cv 1532	. . . 4 class 𝑗
6	5	cuni 4831	. . 3 class ∪ 𝑗
7		vx	. . . . . 6 setvar 𝑥
8		vp	. . . . . 6 setvar 𝑝
9		cvv 3494	. . . . . 6 class V
10	7	cv 1532	. . . . . . . . . 10 class 𝑥
11		c1st 7681	. . . . . . . . . 10 class 1st
12	10, 11	cfv 6349	. . . . . . . . 9 class (1st ‘𝑥)
13		ctopn 16689	. . . . . . . . 9 class TopOpen
14	12, 13	cfv 6349	. . . . . . . 8 class (TopOpen‘(1st ‘𝑥))
15		c2nd 7682	. . . . . . . . 9 class 2nd
16	10, 15	cfv 6349	. . . . . . . 8 class (2nd ‘𝑥)
17		comi 23599	. . . . . . . 8 class Ω1
18	14, 16, 17	co 7150	. . . . . . 7 class ((TopOpen‘(1st ‘𝑥)) Ω1 (2nd ‘𝑥))
19		cc0 10531	. . . . . . . . 9 class 0
20		c1 10532	. . . . . . . . 9 class 1
21		cicc 12735	. . . . . . . . 9 class [,]
22	19, 20, 21	co 7150	. . . . . . . 8 class (0[,]1)
23	16	csn 4560	. . . . . . . 8 class {(2nd ‘𝑥)}
24	22, 23	cxp 5547	. . . . . . 7 class ((0[,]1) × {(2nd ‘𝑥)})
25	18, 24	cop 4566	. . . . . 6 class ⟨((TopOpen‘(1st ‘𝑥)) Ω1 (2nd ‘𝑥)), ((0[,]1) × {(2nd ‘𝑥)})⟩
26	7, 8, 9, 9, 25	cmpo 7152	. . . . 5 class (𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st ‘𝑥)) Ω1 (2nd ‘𝑥)), ((0[,]1) × {(2nd ‘𝑥)})⟩)
27	26, 11	ccom 5553	. . . 4 class ((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st ‘𝑥)) Ω1 (2nd ‘𝑥)), ((0[,]1) × {(2nd ‘𝑥)})⟩) ∘ 1st )
28		cnx 16474	. . . . . . . 8 class ndx
29		cbs 16477	. . . . . . . 8 class Base
30	28, 29	cfv 6349	. . . . . . 7 class (Base‘ndx)
31	30, 6	cop 4566	. . . . . 6 class ⟨(Base‘ndx), ∪ 𝑗⟩
32		cts 16565	. . . . . . . 8 class TopSet
33	28, 32	cfv 6349	. . . . . . 7 class (TopSet‘ndx)
34	33, 5	cop 4566	. . . . . 6 class ⟨(TopSet‘ndx), 𝑗⟩
35	31, 34	cpr 4562	. . . . 5 class {⟨(Base‘ndx), ∪ 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}
36	3	cv 1532	. . . . 5 class 𝑦
37	35, 36	cop 4566	. . . 4 class ⟨{⟨(Base‘ndx), ∪ 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦⟩
38	27, 37, 19	cseq 13363	. . 3 class seq0(((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st ‘𝑥)) Ω1 (2nd ‘𝑥)), ((0[,]1) × {(2nd ‘𝑥)})⟩) ∘ 1st ), ⟨{⟨(Base‘ndx), ∪ 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦⟩)
39	2, 3, 4, 6, 38	cmpo 7152	. 2 class (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ seq0(((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st ‘𝑥)) Ω1 (2nd ‘𝑥)), ((0[,]1) × {(2nd ‘𝑥)})⟩) ∘ 1st ), ⟨{⟨(Base‘ndx), ∪ 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦⟩))
40	1, 39	wceq 1533	1 wff Ω𝑛 = (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ seq0(((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st ‘𝑥)) Ω1 (2nd ‘𝑥)), ((0[,]1) × {(2nd ‘𝑥)})⟩) ∘ 1st ), ⟨{⟨(Base‘ndx), ∪ 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦⟩))

This definition is referenced by: (None)