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	|- G = ( EndoFMnd ` A )
	efmnd1bas.2	|- B = ( Base ` G )
	efmnd2bas.0	|- A = { I , J }
Assertion	efmnd2hash	|- ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` B ) = 4 )

Proof

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 } e. Fin
5	3 4	eqeltri	|- A e. Fin
6	1 2	efmndhash	|- ( A e. Fin -> ( # ` B ) = ( ( # ` A ) ^ ( # ` A ) ) )
7	5 6	ax-mp	|- ( # ` B ) = ( ( # ` A ) ^ ( # ` A ) )
8	3	fveq2i	|- ( # ` A ) = ( # ` { I , J } )
9		elex	|- ( I e. V -> I e. _V )
10		elex	|- ( J e. W -> J e. _V )
11		id	|- ( I =/= J -> I =/= J )
12	9 10 11	3anim123i	|- ( ( I e. V /\ J e. W /\ I =/= J ) -> ( I e. _V /\ J e. _V /\ I =/= J ) )
13		hashprb	|- ( ( I e. _V /\ J e. _V /\ I =/= J ) <-> ( # ` { I , J } ) = 2 )
14	12 13	sylib	|- ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` { I , J } ) = 2 )
15	8 14	syl5eq	|- ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` A ) = 2 )
16	15 15	oveq12d	|- ( ( I e. V /\ J e. W /\ I =/= J ) -> ( ( # ` A ) ^ ( # ` A ) ) = ( 2 ^ 2 ) )
17		sq2	|- ( 2 ^ 2 ) = 4
18	16 17	eqtrdi	|- ( ( I e. V /\ J e. W /\ I =/= J ) -> ( ( # ` A ) ^ ( # ` A ) ) = 4 )
19	7 18	syl5eq	|- ( ( I e. V /\ J e. W /\ I =/= J ) -> ( # ` B ) = 4 )