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 X ) ~~ ( Base ` ( EndoFMnd ` X ) )

Proof

Step Hyp Ref Expression
1 1aryenef 
 |-  ( 1 -aryF X ) ~~ ( X ^m X )
2 eqid 
 |-  ( EndoFMnd ` X ) = ( EndoFMnd ` X )
3 eqid 
 |-  ( Base ` ( EndoFMnd ` X ) ) = ( Base ` ( EndoFMnd ` X ) )
4 2 3 efmndbas 
 |-  ( Base ` ( EndoFMnd ` X ) ) = ( X ^m X )
5 1 4 breqtrri 
 |-  ( 1 -aryF X ) ~~ ( Base ` ( EndoFMnd ` X ) )