efmnd1bas

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

Step	Hyp	Ref	Expression
1		efmnd1bas.1	$⊢ G = EndoFMnd (A)$
2		efmnd1bas.2	$⊢ B = {Base}_{G}$
3		efmnd1bas.0	$⊢ A = \{I\}$
4	3	fveq2i	$⊢ EndoFMnd (A) = EndoFMnd (\{I\})$
5	1 4	eqtri	$⊢ G = EndoFMnd (\{I\})$
6	5 2	efmndbas	$⊢ B = {\{I\}}^{\{I\}}$
7		fsng	$⊢ (I \in V \land I \in V) \to (p : \{I\} ⟶ \{I\} \leftrightarrow p = \{⟨I, I⟩\})$
8	7	anidms	$⊢ I \in V \to (p : \{I\} ⟶ \{I\} \leftrightarrow p = \{⟨I, I⟩\})$
9		snex	$⊢ \{I\} \in V$
10	9 9	elmap	$⊢ p \in ({\{I\}}^{\{I\}}) \leftrightarrow p : \{I\} ⟶ \{I\}$
11		velsn	$⊢ p \in \{\{⟨I, I⟩\}\} \leftrightarrow p = \{⟨I, I⟩\}$
12	8 10 11	3bitr4g	$⊢ I \in V \to (p \in ({\{I\}}^{\{I\}}) \leftrightarrow p \in \{\{⟨I, I⟩\}\})$
13	12	eqrdv	$⊢ I \in V \to {\{I\}}^{\{I\}} = \{\{⟨I, I⟩\}\}$
14	6 13	eqtrid	$⊢ I \in V \to B = \{\{⟨I, I⟩\}\}$

Metamath Proof Explorer