Metamath Proof Explorer


Theorem efmndbasfi

Description: The monoid of endofunctions on a finite set A is finite. (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypotheses efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
Assertion efmndbasfi ( 𝐴 ∈ Fin → 𝐵 ∈ Fin )

Proof

Step Hyp Ref Expression
1 efmndbas.g 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 efmndbas.b 𝐵 = ( Base ‘ 𝐺 )
3 1 2 efmndbas 𝐵 = ( 𝐴m 𝐴 )
4 mapfi ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( 𝐴m 𝐴 ) ∈ Fin )
5 4 anidms ( 𝐴 ∈ Fin → ( 𝐴m 𝐴 ) ∈ Fin )
6 3 5 eqeltrid ( 𝐴 ∈ Fin → 𝐵 ∈ Fin )