Theorem hashfac

Description: A factorial counts the number of bijections on a finite set. (Contributed by Mario Carneiro, 21-Jan-2015) (Proof shortened by Mario Carneiro, 17-Apr-2015)

	Ref	Expression
Assertion	hashfac	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hashf1	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) ) )
2	1	anidms	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) ) )
3		enrefg	⊢ ( 𝐴 ∈ Fin → 𝐴 ≈ 𝐴 )
4		f1finf1o	⊢ ( ( 𝐴 ≈ 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝑓 : 𝐴 –1-1→ 𝐴 ↔ 𝑓 : 𝐴 –1-1-onto→ 𝐴 ) )
5	3 4	mpancom	⊢ ( 𝐴 ∈ Fin → ( 𝑓 : 𝐴 –1-1→ 𝐴 ↔ 𝑓 : 𝐴 –1-1-onto→ 𝐴 ) )
6	5	abbidv	⊢ ( 𝐴 ∈ Fin → { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } )
7	6	fveq2d	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐴 } ) = ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) )
8		hashcl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
9		bcnn	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) = 1 )
10	8 9	syl	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) = 1 )
11	10	oveq2d	⊢ ( 𝐴 ∈ Fin → ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · 1 ) )
12	8	faccld	⊢ ( 𝐴 ∈ Fin → ( ! ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℕ )
13	12	nncnd	⊢ ( 𝐴 ∈ Fin → ( ! ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℂ )
14	13	mulridd	⊢ ( 𝐴 ∈ Fin → ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · 1 ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )
15	11 14	eqtrd	⊢ ( 𝐴 ∈ Fin → ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐴 ) C ( ♯ ‘ 𝐴 ) ) ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )
16	2 7 15	3eqtr3d	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )