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 No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
Assertion efmndtset A V 𝑡 A × 𝒫 A = TopSet G

Proof

Step Hyp Ref Expression
1 efmndtset.g Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2 fvex 𝑡 A × 𝒫 A V
3 eqid Base ndx A A + ndx f A A , g A A f g TopSet ndx 𝑡 A × 𝒫 A = Base ndx A A + ndx f A A , g A A f g TopSet ndx 𝑡 A × 𝒫 A
4 3 topgrptset 𝑡 A × 𝒫 A V 𝑡 A × 𝒫 A = TopSet Base ndx A A + ndx f A A , g A A f g TopSet ndx 𝑡 A × 𝒫 A
5 2 4 ax-mp 𝑡 A × 𝒫 A = TopSet Base ndx A A + ndx f A A , g A A f g TopSet ndx 𝑡 A × 𝒫 A
6 eqid A A = A A
7 eqid f A A , g A A f g = f A A , g A A f g
8 eqid 𝑡 A × 𝒫 A = 𝑡 A × 𝒫 A
9 1 6 7 8 efmnd A V G = Base ndx A A + ndx f A A , g A A f g TopSet ndx 𝑡 A × 𝒫 A
10 9 fveq2d A V TopSet G = TopSet Base ndx A A + ndx f A A , g A A f g TopSet ndx 𝑡 A × 𝒫 A
11 5 10 eqtr4id A V 𝑡 A × 𝒫 A = TopSet G