Metamath Proof Explorer


Theorem om1tset

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 ( 𝜑𝑌𝑋 )
Assertion om1tset ( 𝜑 → ( 𝐽ko II ) = ( TopSet ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 om1bas.o 𝑂 = ( 𝐽 Ω1 𝑌 )
2 om1bas.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 om1bas.y ( 𝜑𝑌𝑋 )
4 ovex ( 𝐽ko II ) ∈ V
5 eqid { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽ko II ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽ko II ) ⟩ }
6 5 topgrptset ( ( 𝐽ko II ) ∈ V → ( 𝐽ko II ) = ( TopSet ‘ { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽ko II ) ⟩ } ) )
7 4 6 ax-mp ( 𝐽ko II ) = ( TopSet ‘ { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽ko II ) ⟩ } )
8 eqidd ( 𝜑 → ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 ) )
9 1 2 3 8 om1bas ( 𝜑 → ( Base ‘ 𝑂 ) = { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } )
10 eqidd ( 𝜑 → ( *𝑝𝐽 ) = ( *𝑝𝐽 ) )
11 eqidd ( 𝜑 → ( 𝐽ko II ) = ( 𝐽ko II ) )
12 1 9 10 11 2 3 om1val ( 𝜑𝑂 = { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽ko II ) ⟩ } )
13 12 fveq2d ( 𝜑 → ( TopSet ‘ 𝑂 ) = ( TopSet ‘ { ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( *𝑝𝐽 ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( 𝐽ko II ) ⟩ } ) )
14 7 13 eqtr4id ( 𝜑 → ( 𝐽ko II ) = ( TopSet ‘ 𝑂 ) )