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 
|- G = ( EndoFMnd ` A )
Assertion efmndtset 
|- ( A e. V -> ( Xt_ ` ( A X. { ~P A } ) ) = ( TopSet ` G ) )

Proof

Step Hyp Ref Expression
1 efmndtset.g 
 |-  G = ( EndoFMnd ` A )
2 fvex 
 |-  ( Xt_ ` ( A X. { ~P A } ) ) e. _V
3 eqid 
 |-  { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } = { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. }
4 3 topgrptset 
 |-  ( ( Xt_ ` ( A X. { ~P A } ) ) e. _V -> ( Xt_ ` ( A X. { ~P A } ) ) = ( TopSet ` { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } ) )
5 2 4 ax-mp 
 |-  ( Xt_ ` ( A X. { ~P A } ) ) = ( TopSet ` { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } )
6 eqid 
 |-  ( A ^m A ) = ( A ^m A )
7 eqid 
 |-  ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) = ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) )
8 eqid 
 |-  ( Xt_ ` ( A X. { ~P A } ) ) = ( Xt_ ` ( A X. { ~P A } ) )
9 1 6 7 8 efmnd 
 |-  ( A e. V -> G = { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } )
10 9 fveq2d 
 |-  ( A e. V -> ( TopSet ` G ) = ( TopSet ` { <. ( Base ` ndx ) , ( A ^m A ) >. , <. ( +g ` ndx ) , ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } ) )
11 5 10 eqtr4id 
 |-  ( A e. V -> ( Xt_ ` ( A X. { ~P A } ) ) = ( TopSet ` G ) )