Theorem om1opn

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

	Ref	Expression
Hypotheses	om1bas.o	|- O = ( J Om1 Y )
	om1bas.j	|- ( ph -> J e. ( TopOn ` X ) )
	om1bas.y	|- ( ph -> Y e. X )
	om1opn.k	|- K = ( TopOpen ` O )
	om1opn.b	|- ( ph -> B = ( Base ` O ) )
Assertion	om1opn	|- ( ph -> K = ( ( J ^ko II ) |`t B ) )

Proof

Step	Hyp	Ref	Expression
1		om1bas.o	|- O = ( J Om1 Y )
2		om1bas.j	|- ( ph -> J e. ( TopOn ` X ) )
3		om1bas.y	|- ( ph -> Y e. X )
4		om1opn.k	|- K = ( TopOpen ` O )
5		om1opn.b	|- ( ph -> B = ( Base ` O ) )
6		eqid	|- ( Base ` O ) = ( Base ` O )
7		eqid	|- ( TopSet ` O ) = ( TopSet ` O )
8	6 7	topnval	|- ( ( TopSet ` O ) |`t ( Base ` O ) ) = ( TopOpen ` O )
9	4 8	eqtr4i	|- K = ( ( TopSet ` O ) |`t ( Base ` O ) )
10	1 2 3	om1tset	|- ( ph -> ( J ^ko II ) = ( TopSet ` O ) )
11	10 5	oveq12d	|- ( ph -> ( ( J ^ko II ) |`t B ) = ( ( TopSet ` O ) |`t ( Base ` O ) ) )
12	9 11	eqtr4id	|- ( ph -> K = ( ( J ^ko II ) |`t B ) )