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

Definition df-omn 22615
 Description: Define the n-th iterated loop space of a topological space. Unlike Ω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 Ω𝑛 = (𝑗 ∈ 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
StepHypRef Expression
1 comn 22610 . 2 class Ω𝑛
2 vj . . 3 setvar 𝑗
3 vy . . 3 setvar 𝑦
4 ctop 20517 . . 3 class Top
52cv 1474 . . . 4 class 𝑗
65cuni 4372 . . 3 class 𝑗
7 vx . . . . . 6 setvar 𝑥
8 vp . . . . . 6 setvar 𝑝
9 cvv 3173 . . . . . 6 class V
107cv 1474 . . . . . . . . . 10 class 𝑥
11 c1st 7057 . . . . . . . . . 10 class 1st
1210, 11cfv 5804 . . . . . . . . 9 class (1st𝑥)
13 ctopn 15905 . . . . . . . . 9 class TopOpen
1412, 13cfv 5804 . . . . . . . 8 class (TopOpen‘(1st𝑥))
15 c2nd 7058 . . . . . . . . 9 class 2nd
1610, 15cfv 5804 . . . . . . . 8 class (2nd𝑥)
17 comi 22609 . . . . . . . 8 class Ω1
1814, 16, 17co 6549 . . . . . . 7 class ((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥))
19 cc0 9815 . . . . . . . . 9 class 0
20 c1 9816 . . . . . . . . 9 class 1
21 cicc 12049 . . . . . . . . 9 class [,]
2219, 20, 21co 6549 . . . . . . . 8 class (0[,]1)
2316csn 4125 . . . . . . . 8 class {(2nd𝑥)}
2422, 23cxp 5036 . . . . . . 7 class ((0[,]1) × {(2nd𝑥)})
2518, 24cop 4131 . . . . . 6 class ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩
267, 8, 9, 9, 25cmpt2 6551 . . . . 5 class (𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩)
2726, 11ccom 5042 . . . 4 class ((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩) ∘ 1st )
28 cnx 15692 . . . . . . . 8 class ndx
29 cbs 15695 . . . . . . . 8 class Base
3028, 29cfv 5804 . . . . . . 7 class (Base‘ndx)
3130, 6cop 4131 . . . . . 6 class ⟨(Base‘ndx), 𝑗
32 cts 15774 . . . . . . . 8 class TopSet
3328, 32cfv 5804 . . . . . . 7 class (TopSet‘ndx)
3433, 5cop 4131 . . . . . 6 class ⟨(TopSet‘ndx), 𝑗
3531, 34cpr 4127 . . . . 5 class {⟨(Base‘ndx), 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}
363cv 1474 . . . . 5 class 𝑦
3735, 36cop 4131 . . . 4 class ⟨{⟨(Base‘ndx), 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦
3827, 37, 19cseq 12663 . . 3 class seq0(((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩) ∘ 1st ), ⟨{⟨(Base‘ndx), 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦⟩)
392, 3, 4, 6, 38cmpt2 6551 . 2 class (𝑗 ∈ Top, 𝑦 𝑗 ↦ seq0(((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩) ∘ 1st ), ⟨{⟨(Base‘ndx), 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦⟩))
401, 39wceq 1475 1 wff Ω𝑛 = (𝑗 ∈ Top, 𝑦 𝑗 ↦ seq0(((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩) ∘ 1st ), ⟨{⟨(Base‘ndx), 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦⟩))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator