Theorem efmnd2hash

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

	Ref	Expression
Hypotheses	efmnd1bas.1	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
	efmnd1bas.2	$$⊢B={\mathrm{Base}}_G$$
	efmnd2bas.0	$$⊢A=\left\{I,J\right\}$$
Assertion	efmnd2hash	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|B\right|=4$$

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={\mathrm{Base}}_G$$
3		efmnd2bas.0	$$⊢A=\left\{I,J\right\}$$
4		prfi	$$⊢\left\{I,J\right\}\in \mathrm{Fin}$$
5	3 4	eqeltri	$$⊢A\in \mathrm{Fin}$$
6	1 2	efmndhash	$$⊢A\in \mathrm{Fin}\to \left|B\right|={\left|A\right|}^{\left|A\right|}$$
7	5 6	ax-mp	$$⊢\left|B\right|={\left|A\right|}^{\left|A\right|}$$
8	3	fveq2i	$$⊢\left|A\right|=\left|\left\{I,J\right\}\right|$$
9		elex	$$⊢I\in V\to I\in \mathrm{V}$$
10		elex	$$⊢J\in W\to J\in \mathrm{V}$$
11		id	$$⊢I\ne J\to I\ne J$$
12	9 10 11	3anim123i	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left(I\in \mathrm{V}\wedge J\in \mathrm{V}\wedge I\ne J\right)$$
13		hashprb	$$⊢\left(I\in \mathrm{V}\wedge J\in \mathrm{V}\wedge I\ne J\right)\leftrightarrow \left|\left\{I,J\right\}\right|=2$$
14	12 13	sylib	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|\left\{I,J\right\}\right|=2$$
15	8 14	syl5eq	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|A\right|=2$$
16	15 15	oveq12d	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to {\left|A\right|}^{\left|A\right|}=2^2$$
17		sq2	$$⊢2^2=4$$
18	16 17	syl6eq	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to {\left|A\right|}^{\left|A\right|}=4$$
19	7 18	syl5eq	$$⊢\left(I\in V\wedge J\in W\wedge I\ne J\right)\to \left|B\right|=4$$