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 ( 1 -aryF 𝑋 ) ≈ ( Base ‘ ( EndoFMnd ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 1aryenef ( 1 -aryF 𝑋 ) ≈ ( 𝑋m 𝑋 )
2 eqid ( EndoFMnd ‘ 𝑋 ) = ( EndoFMnd ‘ 𝑋 )
3 eqid ( Base ‘ ( EndoFMnd ‘ 𝑋 ) ) = ( Base ‘ ( EndoFMnd ‘ 𝑋 ) )
4 2 3 efmndbas ( Base ‘ ( EndoFMnd ‘ 𝑋 ) ) = ( 𝑋m 𝑋 )
5 1 4 breqtrri ( 1 -aryF 𝑋 ) ≈ ( Base ‘ ( EndoFMnd ‘ 𝑋 ) )