Metamath Proof Explorer


Theorem efmndtset

Description: The topology of the monoid of endofunctions on A . This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just endofunctions - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by AV, 25-Jan-2024)

Ref Expression
Hypothesis efmndtset.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
Assertion efmndtset ( 𝐴𝑉 → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 efmndtset.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 fvex ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ∈ V
3 eqid { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ }
4 3 topgrptset ( ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ∈ V → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } ) )
5 2 4 ax-mp ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } )
6 eqid ( 𝐴m 𝐴 ) = ( 𝐴m 𝐴 )
7 eqid ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) = ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) )
8 eqid ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) )
9 1 6 7 8 efmnd ( 𝐴𝑉𝐺 = { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } )
10 9 fveq2d ( 𝐴𝑉 → ( TopSet ‘ 𝐺 ) = ( TopSet ‘ { ⟨ ( Base ‘ ndx ) , ( 𝐴m 𝐴 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ⟩ } ) )
11 5 10 eqtr4id ( 𝐴𝑉 → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ 𝐺 ) )