Theorem om1opn

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$$
	om1opn.k	$$⊢K=\mathrm{TopOpen}\left(O\right)$$
	om1opn.b	$$⊢\phi \to B={\mathrm{Base}}_O$$
Assertion	om1opn	$$⊢\phi \to K=\left(J{^}_{\mathrm{ko}}\mathrm{II}\right){\upharpoonright }_{𝑡}B$$

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		om1opn.k	$$⊢K=\mathrm{TopOpen}\left(O\right)$$
5		om1opn.b	$$⊢\phi \to B={\mathrm{Base}}_O$$
6		eqid	$$⊢{\mathrm{Base}}_O={\mathrm{Base}}_O$$
7		eqid	$$⊢\mathrm{TopSet}\left(O\right)=\mathrm{TopSet}\left(O\right)$$
8	6 7	topnval	$$⊢\mathrm{TopSet}\left(O\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_O=\mathrm{TopOpen}\left(O\right)$$
9	4 8	eqtr4i	$$⊢K=\mathrm{TopSet}\left(O\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_O$$
10	1 2 3	om1tset	$$⊢\phi \to J{^}_{\mathrm{ko}}\mathrm{II}=\mathrm{TopSet}\left(O\right)$$
11	10 5	oveq12d	$$⊢\phi \to \left(J{^}_{\mathrm{ko}}\mathrm{II}\right){\upharpoonright }_{𝑡}B=\mathrm{TopSet}\left(O\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_O$$
12	9 11	eqtr4id	$$⊢\phi \to K=\left(J{^}_{\mathrm{ko}}\mathrm{II}\right){\upharpoonright }_{𝑡}B$$