Metamath Proof Explorer


Theorem efmnd1bas

Description: The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024)

Ref Expression
Hypotheses efmnd1bas.1 No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
efmnd1bas.2 B = Base G
efmnd1bas.0 A = I
Assertion efmnd1bas I V B = I I

Proof

Step Hyp Ref Expression
1 efmnd1bas.1 Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2 efmnd1bas.2 B = Base G
3 efmnd1bas.0 A = I
4 3 fveq2i Could not format ( EndoFMnd ` A ) = ( EndoFMnd ` { I } ) : No typesetting found for |- ( EndoFMnd ` A ) = ( EndoFMnd ` { I } ) with typecode |-
5 1 4 eqtri Could not format G = ( EndoFMnd ` { I } ) : No typesetting found for |- G = ( EndoFMnd ` { I } ) with typecode |-
6 5 2 efmndbas B = I I
7 fsng I V I V p : I I p = I I
8 7 anidms I V p : I I p = I I
9 snex I V
10 9 9 elmap p I I p : I I
11 velsn p I I p = I I
12 8 10 11 3bitr4g I V p I I p I I
13 12 eqrdv I V I I = I I
14 6 13 syl5eq I V B = I I