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 syl5eq 
 |-  ( -. 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 )