This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )