Metamath Proof Explorer


Theorem 1aryenefmnd

Description: The set of unary (endo)functions and the base set of the monoid of endofunctions are equinumerous. (Contributed by AV, 19-May-2024)

Ref Expression
Assertion 1aryenefmnd Could not format assertion : No typesetting found for |- ( 1 -aryF X ) ~~ ( Base ` ( EndoFMnd ` X ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 1aryenef Could not format ( 1 -aryF X ) ~~ ( X ^m X ) : No typesetting found for |- ( 1 -aryF X ) ~~ ( X ^m X ) with typecode |-
2 eqid Could not format ( EndoFMnd ` X ) = ( EndoFMnd ` X ) : No typesetting found for |- ( EndoFMnd ` X ) = ( EndoFMnd ` X ) with typecode |-
3 eqid Could not format ( Base ` ( EndoFMnd ` X ) ) = ( Base ` ( EndoFMnd ` X ) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` X ) ) = ( Base ` ( EndoFMnd ` X ) ) with typecode |-
4 2 3 efmndbas Could not format ( Base ` ( EndoFMnd ` X ) ) = ( X ^m X ) : No typesetting found for |- ( Base ` ( EndoFMnd ` X ) ) = ( X ^m X ) with typecode |-
5 1 4 breqtrri Could not format ( 1 -aryF X ) ~~ ( Base ` ( EndoFMnd ` X ) ) : No typesetting found for |- ( 1 -aryF X ) ~~ ( Base ` ( EndoFMnd ` X ) ) with typecode |-