Theorem om1opn

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

	Ref	Expression
Hypotheses	om1bas.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
	om1bas.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	om1bas.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
	om1opn.k	⊢ 𝐾 = ( TopOpen ‘ 𝑂 )
	om1opn.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑂 ) )
Assertion	om1opn	⊢ ( 𝜑 → 𝐾 = ( ( 𝐽 ↑ko II ) ↾t 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		om1bas.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
2		om1bas.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		om1bas.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
4		om1opn.k	⊢ 𝐾 = ( TopOpen ‘ 𝑂 )
5		om1opn.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑂 ) )
6		eqid	⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
7		eqid	⊢ ( TopSet ‘ 𝑂 ) = ( TopSet ‘ 𝑂 )
8	6 7	topnval	⊢ ( ( TopSet ‘ 𝑂 ) ↾t ( Base ‘ 𝑂 ) ) = ( TopOpen ‘ 𝑂 )
9	4 8	eqtr4i	⊢ 𝐾 = ( ( TopSet ‘ 𝑂 ) ↾t ( Base ‘ 𝑂 ) )
10	1 2 3	om1tset	⊢ ( 𝜑 → ( 𝐽 ↑ko II ) = ( TopSet ‘ 𝑂 ) )
11	10 5	oveq12d	⊢ ( 𝜑 → ( ( 𝐽 ↑ko II ) ↾t 𝐵 ) = ( ( TopSet ‘ 𝑂 ) ↾t ( Base ‘ 𝑂 ) ) )
12	9 11	eqtr4id	⊢ ( 𝜑 → 𝐾 = ( ( 𝐽 ↑ko II ) ↾t 𝐵 ) )