Metamath Proof Explorer


Theorem efmndbas

Description: The base set of the monoid of endofunctions on class A . (Contributed by AV, 25-Jan-2024)

Ref Expression
Hypotheses efmndbas.g
|- G = ( EndoFMnd ` A )
efmndbas.b
|- B = ( Base ` G )
Assertion efmndbas
|- B = ( A ^m A )

Proof

Step Hyp Ref Expression
1 efmndbas.g
 |-  G = ( EndoFMnd ` A )
2 efmndbas.b
 |-  B = ( Base ` G )
3 ovex
 |-  ( A ^m A ) e. _V
4 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 } ) ) >. }
5 4 topgrpbas
 |-  ( ( A ^m A ) e. _V -> ( A ^m A ) = ( Base ` { <. ( 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 3 5 mp1i
 |-  ( A e. _V -> ( A ^m A ) = ( Base ` { <. ( 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 } ) ) >. } ) )
7 eqid
 |-  ( A ^m A ) = ( A ^m A )
8 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 ) )
9 eqid
 |-  ( Xt_ ` ( A X. { ~P A } ) ) = ( Xt_ ` ( A X. { ~P A } ) )
10 1 7 8 9 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 } ) ) >. } )
11 10 fveq2d
 |-  ( A e. _V -> ( Base ` G ) = ( Base ` { <. ( 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 } ) ) >. } ) )
12 6 11 eqtr4d
 |-  ( A e. _V -> ( A ^m A ) = ( Base ` G ) )
13 base0
 |-  (/) = ( Base ` (/) )
14 reldmmap
 |-  Rel dom ^m
15 14 ovprc1
 |-  ( -. A e. _V -> ( A ^m A ) = (/) )
16 fvprc
 |-  ( -. A e. _V -> ( EndoFMnd ` A ) = (/) )
17 1 16 eqtrid
 |-  ( -. A e. _V -> G = (/) )
18 17 fveq2d
 |-  ( -. A e. _V -> ( Base ` G ) = ( Base ` (/) ) )
19 13 15 18 3eqtr4a
 |-  ( -. A e. _V -> ( A ^m A ) = ( Base ` G ) )
20 12 19 pm2.61i
 |-  ( A ^m A ) = ( Base ` G )
21 2 20 eqtr4i
 |-  B = ( A ^m A )