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

Definition df-omn 23612
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 23607 . 2 class Ω𝑛
2 vj . . 3 setvar 𝑗
3 vy . . 3 setvar 𝑦
4 ctop 21498 . . 3 class Top
52cv 1537 . . . 4 class 𝑗
65cuni 4800 . . 3 class 𝑗
7 vx . . . . . 6 setvar 𝑥
8 vp . . . . . 6 setvar 𝑝
9 cvv 3441 . . . . . 6 class V
107cv 1537 . . . . . . . . . 10 class 𝑥
11 c1st 7669 . . . . . . . . . 10 class 1st
1210, 11cfv 6324 . . . . . . . . 9 class (1st𝑥)
13 ctopn 16687 . . . . . . . . 9 class TopOpen
1412, 13cfv 6324 . . . . . . . 8 class (TopOpen‘(1st𝑥))
15 c2nd 7670 . . . . . . . . 9 class 2nd
1610, 15cfv 6324 . . . . . . . 8 class (2nd𝑥)
17 comi 23606 . . . . . . . 8 class Ω1
1814, 16, 17co 7135 . . . . . . 7 class ((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥))
19 cc0 10526 . . . . . . . . 9 class 0
20 c1 10527 . . . . . . . . 9 class 1
21 cicc 12729 . . . . . . . . 9 class [,]
2219, 20, 21co 7135 . . . . . . . 8 class (0[,]1)
2316csn 4525 . . . . . . . 8 class {(2nd𝑥)}
2422, 23cxp 5517 . . . . . . 7 class ((0[,]1) × {(2nd𝑥)})
2518, 24cop 4531 . . . . . 6 class ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩
267, 8, 9, 9, 25cmpo 7137 . . . . 5 class (𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩)
2726, 11ccom 5523 . . . 4 class ((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩) ∘ 1st )
28 cnx 16472 . . . . . . . 8 class ndx
29 cbs 16475 . . . . . . . 8 class Base
3028, 29cfv 6324 . . . . . . 7 class (Base‘ndx)
3130, 6cop 4531 . . . . . 6 class ⟨(Base‘ndx), 𝑗
32 cts 16563 . . . . . . . 8 class TopSet
3328, 32cfv 6324 . . . . . . 7 class (TopSet‘ndx)
3433, 5cop 4531 . . . . . 6 class ⟨(TopSet‘ndx), 𝑗
3531, 34cpr 4527 . . . . 5 class {⟨(Base‘ndx), 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}
363cv 1537 . . . . 5 class 𝑦
3735, 36cop 4531 . . . 4 class ⟨{⟨(Base‘ndx), 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦
3827, 37, 19cseq 13364 . . 3 class seq0(((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩) ∘ 1st ), ⟨{⟨(Base‘ndx), 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦⟩)
392, 3, 4, 6, 38cmpo 7137 . 2 class (𝑗 ∈ Top, 𝑦 𝑗 ↦ seq0(((𝑥 ∈ V, 𝑝 ∈ V ↦ ⟨((TopOpen‘(1st𝑥)) Ω1 (2nd𝑥)), ((0[,]1) × {(2nd𝑥)})⟩) ∘ 1st ), ⟨{⟨(Base‘ndx), 𝑗⟩, ⟨(TopSet‘ndx), 𝑗⟩}, 𝑦⟩))
401, 39wceq 1538 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