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	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
	efmnd1bas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
	efmnd2bas.0	⊢ 𝐴 = { 𝐼 , 𝐽 }
Assertion	efmnd2hash	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ♯ ‘ 𝐵 ) = 4 )

Proof

Step	Hyp	Ref	Expression
1		efmnd1bas.1	⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
2		efmnd1bas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		efmnd2bas.0	⊢ 𝐴 = { 𝐼 , 𝐽 }
4		prfi	⊢ { 𝐼 , 𝐽 } ∈ Fin
5	3 4	eqeltri	⊢ 𝐴 ∈ Fin
6	1 2	efmndhash	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) )
7	5 6	ax-mp	⊢ ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) )
8	3	fveq2i	⊢ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { 𝐼 , 𝐽 } )
9		elex	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ V )
10		elex	⊢ ( 𝐽 ∈ 𝑊 → 𝐽 ∈ V )
11		id	⊢ ( 𝐼 ≠ 𝐽 → 𝐼 ≠ 𝐽 )
12	9 10 11	3anim123i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( 𝐼 ∈ V ∧ 𝐽 ∈ V ∧ 𝐼 ≠ 𝐽 ) )
13		hashprb	⊢ ( ( 𝐼 ∈ V ∧ 𝐽 ∈ V ∧ 𝐼 ≠ 𝐽 ) ↔ ( ♯ ‘ { 𝐼 , 𝐽 } ) = 2 )
14	12 13	sylib	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ♯ ‘ { 𝐼 , 𝐽 } ) = 2 )
15	8 14	syl5eq	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ♯ ‘ 𝐴 ) = 2 )
16	15 15	oveq12d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) = ( 2 ↑ 2 ) )
17		sq2	⊢ ( 2 ↑ 2 ) = 4
18	16 17	eqtrdi	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ( ♯ ‘ 𝐴 ) ↑ ( ♯ ‘ 𝐴 ) ) = 4 )
19	7 18	syl5eq	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ♯ ‘ 𝐵 ) = 4 )