Metamath Proof Explorer


Theorem efmndtopn

Description: The topology of the monoid of endofunctions on A . (Contributed by AV, 31-Jan-2024)

Ref Expression
Hypotheses efmndtopn.g No typesetting found for |- G = ( EndoFMnd ` X ) with typecode |-
efmndtopn.b B = Base G
Assertion efmndtopn X V 𝑡 X × 𝒫 X 𝑡 B = TopOpen G

Proof

Step Hyp Ref Expression
1 efmndtopn.g Could not format G = ( EndoFMnd ` X ) : No typesetting found for |- G = ( EndoFMnd ` X ) with typecode |-
2 efmndtopn.b B = Base G
3 1 efmndtset X V 𝑡 X × 𝒫 X = TopSet G
4 3 oveq1d X V 𝑡 X × 𝒫 X 𝑡 B = TopSet G 𝑡 B
5 eqid TopSet G = TopSet G
6 2 5 topnval TopSet G 𝑡 B = TopOpen G
7 4 6 eqtrdi X V 𝑡 X × 𝒫 X 𝑡 B = TopOpen G