Metamath Proof Explorer

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	$⊢ A \in Fin \to \|\{f \| f : A \underset{1-1 onto}{⟶} A\}\| = \|A\|!$

Proof

Step	Hyp	Ref	Expression
1		hashf1	$⊢ (A \in Fin \land A \in Fin) \to \|\{f \| f : A \underset{1-1}{⟶} A\}\| = \|A\|! (\binom{\|A\|}{\|A\|})$
2	1	anidms	$⊢ A \in Fin \to \|\{f \| f : A \underset{1-1}{⟶} A\}\| = \|A\|! (\binom{\|A\|}{\|A\|})$
3		enrefg	$⊢ A \in Fin \to A \approx A$
4		f1finf1o	$⊢ (A \approx A \land A \in Fin) \to (f : A \underset{1-1}{⟶} A \leftrightarrow f : A \underset{1-1 onto}{⟶} A)$
5	3 4	mpancom	$⊢ A \in Fin \to (f : A \underset{1-1}{⟶} A \leftrightarrow f : A \underset{1-1 onto}{⟶} A)$
6	5	abbidv	$⊢ A \in Fin \to \{f \| f : A \underset{1-1}{⟶} A\} = \{f \| f : A \underset{1-1 onto}{⟶} A\}$
7	6	fveq2d	$⊢ A \in Fin \to \|\{f \| f : A \underset{1-1}{⟶} A\}\| = \|\{f \| f : A \underset{1-1 onto}{⟶} A\}\|$
8		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
9		bcnn	$⊢ \|A\| \in ℕ_{0} \to (\binom{\|A\|}{\|A\|}) = 1$
10	8 9	syl	$⊢ A \in Fin \to (\binom{\|A\|}{\|A\|}) = 1$
11	10	oveq2d	$⊢ A \in Fin \to \|A\|! (\binom{\|A\|}{\|A\|}) = \|A\|! \cdot 1$
12	8	faccld	$⊢ A \in Fin \to \|A\|! \in ℕ$
13	12	nncnd	$⊢ A \in Fin \to \|A\|! \in ℂ$
14	13	mulid1d	$⊢ A \in Fin \to \|A\|! \cdot 1 = \|A\|!$
15	11 14	eqtrd	$⊢ A \in Fin \to \|A\|! (\binom{\|A\|}{\|A\|}) = \|A\|!$
16	2 7 15	3eqtr3d	$⊢ A \in Fin \to \|\{f \| f : A \underset{1-1 onto}{⟶} A\}\| = \|A\|!$