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