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 ‘ 𝑋 ) ) |
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 ‘ 𝑋 ) ) |