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

Metamath Proof Explorer

Theorem efmnd1hash

Description: The monoid of endofunctions on a singleton has cardinality 1 . (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypotheses efmnd1bas.1 ⊢ G = EndoFMnd ⁡ A
efmnd1bas.2 ⊢ B = Base G
efmnd1bas.0 ⊢ A = I
Assertion efmnd1hash ⊢ I ∈ V → B = 1

Proof

Step Hyp Ref Expression
1 efmnd1bas.1 ⊢ G = EndoFMnd ⁡ A
2 efmnd1bas.2 ⊢ B = Base G
3 efmnd1bas.0 ⊢ A = I
4 snfi ⊢ I ∈ Fin
5 3 4 eqeltri ⊢ A ∈ Fin
6 1 2 efmndhash ⊢ A ∈ Fin → B = A A
7 5 6 ax-mp ⊢ B = A A
8 3 fveq2i ⊢ A = I
9 hashsng ⊢ I ∈ V → I = 1
10 8 9 eqtrid ⊢ I ∈ V → A = 1
11 10 10 oveq12d ⊢ I ∈ V → A A = 1 1
12 1z ⊢ 1 ∈ ℤ
13 1exp ⊢ 1 ∈ ℤ → 1 1 = 1
14 12 13 ax-mp ⊢ 1 1 = 1
15 11 14 eqtrdi ⊢ I ∈ V → A A = 1
16 7 15 eqtrid ⊢ I ∈ V → B = 1