efmnd2hash

Description: The monoid of endofunctions on a (proper) pair has cardinality 4 . (Contributed by AV, 18-Feb-2024)

Step	Hyp	Ref	Expression
1		efmnd1bas.1	$⊢ G = EndoFMnd (A)$
2		efmnd1bas.2	$⊢ B = {Base}_{G}$
3		efmnd2bas.0	$⊢ A = \{I, J\}$
4		prfi	$⊢ \{I, J\} \in Fin$
5	3 4	eqeltri	$⊢ A \in Fin$
6	1 2	efmndhash	$⊢ A \in Fin \to \|B\| = {\|A\|}^{\|A\|}$
7	5 6	ax-mp	$⊢ \|B\| = {\|A\|}^{\|A\|}$
8	3	fveq2i	$⊢ \|A\| = \|\{I, J\}\|$
9		elex	$⊢ I \in V \to I \in V$
10		elex	$⊢ J \in W \to J \in V$
11		id	$⊢ I \neq J \to I \neq J$
12	9 10 11	3anim123i	$⊢ (I \in V \land J \in W \land I \neq J) \to (I \in V \land J \in V \land I \neq J)$
13		hashprb	$⊢ (I \in V \land J \in V \land I \neq J) \leftrightarrow \|\{I, J\}\| = 2$
14	12 13	sylib	$⊢ (I \in V \land J \in W \land I \neq J) \to \|\{I, J\}\| = 2$
15	8 14	eqtrid	$⊢ (I \in V \land J \in W \land I \neq J) \to \|A\| = 2$
16	15 15	oveq12d	$⊢ (I \in V \land J \in W \land I \neq J) \to {\|A\|}^{\|A\|} = 2^{2}$
17		sq2	$⊢ 2^{2} = 4$
18	16 17	eqtrdi	$⊢ (I \in V \land J \in W \land I \neq J) \to {\|A\|}^{\|A\|} = 4$
19	7 18	eqtrid	$⊢ (I \in V \land J \in W \land I \neq J) \to \|B\| = 4$

Metamath Proof Explorer