efmndbasabf

Description: The base set of the monoid of endofunctions on class A is the set of functions from A into itself. (Contributed by AV, 29-Mar-2024)

Step	Hyp	Ref	Expression
1		efmndbas.g	$⊢ G = EndoFMnd (A)$
2		efmndbas.b	$⊢ B = {Base}_{G}$
3	1 2	efmndbas	$⊢ B = A^{A}$
4		mapvalg	$⊢ (A \in V \land A \in V) \to A^{A} = \{f \| f : A ⟶ A\}$
5	4	anidms	$⊢ A \in V \to A^{A} = \{f \| f : A ⟶ A\}$
6	3 5	eqtrid	$⊢ A \in V \to B = \{f \| f : A ⟶ A\}$
7		base0	$⊢ \emptyset = {Base}_{\emptyset}$
8	7	eqcomi	$⊢ {Base}_{\emptyset} = \emptyset$
9		fvprc	$⊢ \neg A \in V \to EndoFMnd (A) = \emptyset$
10	1 9	eqtrid	$⊢ \neg A \in V \to G = \emptyset$
11	10	fveq2d	$⊢ \neg A \in V \to {Base}_{G} = {Base}_{\emptyset}$
12	2 11	eqtrid	$⊢ \neg A \in V \to B = {Base}_{\emptyset}$
13		mapprc	$⊢ \neg A \in V \to \{f \| f : A ⟶ A\} = \emptyset$
14	8 12 13	3eqtr4a	$⊢ \neg A \in V \to B = \{f \| f : A ⟶ A\}$
15	6 14	pm2.61i	$⊢ B = \{f \| f : A ⟶ A\}$

Metamath Proof Explorer