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 No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
efmndbas.b B=BaseG
Assertion efmndbas B=AA

Proof

Step Hyp Ref Expression
1 efmndbas.g Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2 efmndbas.b B=BaseG
3 ovex AAV
4 eqid BasendxAA+ndxfAA,gAAfgTopSetndx𝑡A×𝒫A=BasendxAA+ndxfAA,gAAfgTopSetndx𝑡A×𝒫A
5 4 topgrpbas AAVAA=BaseBasendxAA+ndxfAA,gAAfgTopSetndx𝑡A×𝒫A
6 3 5 mp1i AVAA=BaseBasendxAA+ndxfAA,gAAfgTopSetndx𝑡A×𝒫A
7 eqid AA=AA
8 eqid fAA,gAAfg=fAA,gAAfg
9 eqid 𝑡A×𝒫A=𝑡A×𝒫A
10 1 7 8 9 efmnd AVG=BasendxAA+ndxfAA,gAAfgTopSetndx𝑡A×𝒫A
11 10 fveq2d AVBaseG=BaseBasendxAA+ndxfAA,gAAfgTopSetndx𝑡A×𝒫A
12 6 11 eqtr4d AVAA=BaseG
13 base0 =Base
14 reldmmap Reldom𝑚
15 14 ovprc1 ¬AVAA=
16 fvprc Could not format ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) with typecode |-
17 1 16 eqtrid ¬AVG=
18 17 fveq2d ¬AVBaseG=Base
19 13 15 18 3eqtr4a ¬AVAA=BaseG
20 12 19 pm2.61i AA=BaseG
21 2 20 eqtr4i B=AA