Metamath Proof Explorer

Theorem om1bas

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

Ref Expression
Hypotheses om1bas.o ⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
om1bas.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
om1bas.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
om1bas.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑂 ) )
Assertion om1bas ( 𝜑 → 𝐵 = { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } )

Proof

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