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	$⊢ Ω_{𝑛} = (j \in Top, y \in ⋃ j ⟼ seq 0 (((x \in V, p \in V ⟼ ⟨TopOpen (1^{st} (x)) Ω_{1} 2^{nd} (x), [0, 1] \times \{2^{nd} (x)\}⟩) \circ 1^{st}), ⟨\{⟨{Base}_{ndx}, ⋃ j⟩, ⟨TopSet (ndx), j⟩\}, y⟩))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		comn	$class Ω_{𝑛}$
1		vj	$setvar j$
2		ctop	$class Top$
3		vy	$setvar y$
4	1	cv	$setvar j$
5	4	cuni	$class ⋃ j$
6		cc0	$class 0$
7		vx	$setvar x$
8		cvv	$class V$
9		vp	$setvar p$
10		ctopn	$class TopOpen$
11		c1st	$class 1^{st}$
12	7	cv	$setvar x$
13	12 11	cfv	$class 1^{st} (x)$
14	13 10	cfv	$class TopOpen (1^{st} (x))$
15		comi	$class Ω_{1}$
16		c2nd	$class 2^{nd}$
17	12 16	cfv	$class 2^{nd} (x)$
18	14 17 15	co	$class (TopOpen (1^{st} (x)) Ω_{1} 2^{nd} (x))$
19		cicc	$class [.]$
20		c1	$class 1$
21	6 20 19	co	$class [0, 1]$
22	17	csn	$class \{2^{nd} (x)\}$
23	21 22	cxp	$class ([0, 1] \times \{2^{nd} (x)\})$
24	18 23	cop	$class ⟨TopOpen (1^{st} (x)) Ω_{1} 2^{nd} (x), [0, 1] \times \{2^{nd} (x)\}⟩$
25	7 9 8 8 24	cmpo	$class (x \in V, p \in V ⟼ ⟨TopOpen (1^{st} (x)) Ω_{1} 2^{nd} (x), [0, 1] \times \{2^{nd} (x)\}⟩)$
26	25 11	ccom	$class ((x \in V, p \in V ⟼ ⟨TopOpen (1^{st} (x)) Ω_{1} 2^{nd} (x), [0, 1] \times \{2^{nd} (x)\}⟩) \circ 1^{st})$
27		cbs	$class Base$
28		cnx	$class ndx$
29	28 27	cfv	$class {Base}_{ndx}$
30	29 5	cop	$class ⟨{Base}_{ndx}, ⋃ j⟩$
31		cts	$class TopSet$
32	28 31	cfv	$class TopSet (ndx)$
33	32 4	cop	$class ⟨TopSet (ndx), j⟩$
34	30 33	cpr	$class \{⟨{Base}_{ndx}, ⋃ j⟩, ⟨TopSet (ndx), j⟩\}$
35	3	cv	$setvar y$
36	34 35	cop	$class ⟨\{⟨{Base}_{ndx}, ⋃ j⟩, ⟨TopSet (ndx), j⟩\}, y⟩$
37	26 36 6	cseq	$class seq 0 (((x \in V, p \in V ⟼ ⟨TopOpen (1^{st} (x)) Ω_{1} 2^{nd} (x), [0, 1] \times \{2^{nd} (x)\}⟩) \circ 1^{st}), ⟨\{⟨{Base}_{ndx}, ⋃ j⟩, ⟨TopSet (ndx), j⟩\}, y⟩)$
38	1 3 2 5 37	cmpo	$class (j \in Top, y \in ⋃ j ⟼ seq 0 (((x \in V, p \in V ⟼ ⟨TopOpen (1^{st} (x)) Ω_{1} 2^{nd} (x), [0, 1] \times \{2^{nd} (x)\}⟩) \circ 1^{st}), ⟨\{⟨{Base}_{ndx}, ⋃ j⟩, ⟨TopSet (ndx), j⟩\}, y⟩))$
39	0 38	wceq	$wff Ω_{𝑛} = (j \in Top, y \in ⋃ j ⟼ seq 0 (((x \in V, p \in V ⟼ ⟨TopOpen (1^{st} (x)) Ω_{1} 2^{nd} (x), [0, 1] \times \{2^{nd} (x)\}⟩) \circ 1^{st}), ⟨\{⟨{Base}_{ndx}, ⋃ j⟩, ⟨TopSet (ndx), j⟩\}, y⟩))$

Metamath Proof Explorer

Definition df-omn

Detailed syntax breakdown