Metamath Proof Explorer


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 ) , 𝑗 ⟩ } , 𝑦 ⟩ ) )