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 |-