om1tset

Description: The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015)

Step	Hyp	Ref	Expression
1		om1bas.o	$⊢ O = J Ω_{1} Y$
2		om1bas.j	$⊢ φ \to J \in TopOn (X)$
3		om1bas.y	$⊢ φ \to Y \in X$
4		ovex	$⊢ J^_{ko} II \in V$
5		eqid	$⊢ \{⟨{Base}_{ndx}, {Base}_{O}⟩, ⟨+_{ndx}, _{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\} = \{⟨{Base}_{ndx}, {Base}_{O}⟩, ⟨+_{ndx}, _{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\}$
6	5	topgrptset	$⊢ J^_{ko} II \in V \to J^_{ko} II = TopSet (\{⟨{Base}_{ndx}, {Base}_{O}⟩, ⟨+_{ndx}, *_{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\})$
7	4 6	ax-mp	$⊢ J^_{ko} II = TopSet (\{⟨{Base}_{ndx}, {Base}_{O}⟩, ⟨+_{ndx}, *_{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\})$
8		eqidd	$⊢ φ \to {Base}_{O} = {Base}_{O}$
9	1 2 3 8	om1bas	$⊢ φ \to {Base}_{O} = \{f \in (II Cn J) \| (f (0) = Y \land f (1) = Y)\}$
10		eqidd	$⊢ φ \to _{𝑝} (J) = _{𝑝} (J)$
11		eqidd	$⊢ φ \to J^_{ko} II = J^_{ko} II$
12	1 9 10 11 2 3	om1val	$⊢ φ \to O = \{⟨{Base}_{ndx}, {Base}_{O}⟩, ⟨+_{ndx}, *_{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\}$
13	12	fveq2d	$⊢ φ \to TopSet (O) = TopSet (\{⟨{Base}_{ndx}, {Base}_{O}⟩, ⟨+_{ndx}, *_{𝑝} (J)⟩, ⟨TopSet (ndx), J^_{ko} II⟩\})$
14	7 13	eqtr4id	$⊢ φ \to J^_{ko} II = TopSet (O)$

Metamath Proof Explorer