Theorem om1tset

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

	Ref	Expression
Hypotheses	om1bas.o	$$⊢O=J{\Omega }_{1}Y$$
	om1bas.j	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	om1bas.y	$$⊢\phi \to Y\in X$$
Assertion	om1tset	$$⊢\phi \to J{^}_{\mathrm{ko}}\mathrm{II}=\mathrm{TopSet}\left(O\right)$$

Proof

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