derangen2

Description: Write the derangement number in terms of the subfactorial. (Contributed by Mario Carneiro, 22-Jan-2015)

	Ref	Expression
Hypotheses	derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
	subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
Assertion	derangen2	$⊢ A \in Fin \to D (A) = S (\|A\|)$

Step	Hyp	Ref	Expression
1		derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
2		subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
3		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
4	1 2	subfacval	$⊢ \|A\| \in ℕ_{0} \to S (\|A\|) = D ((1 \dots \|A\|))$
5	3 4	syl	$⊢ A \in Fin \to S (\|A\|) = D ((1 \dots \|A\|))$
6		hashfz1	$⊢ \|A\| \in ℕ_{0} \to \|(1 \dots \|A\|)\| = \|A\|$
7	3 6	syl	$⊢ A \in Fin \to \|(1 \dots \|A\|)\| = \|A\|$
8		fzfid	$⊢ A \in Fin \to (1 \dots \|A\|) \in Fin$
9		hashen	$⊢ ((1 \dots \|A\|) \in Fin \land A \in Fin) \to (\|(1 \dots \|A\|)\| = \|A\| \leftrightarrow (1 \dots \|A\|) \approx A)$
10	8 9	mpancom	$⊢ A \in Fin \to (\|(1 \dots \|A\|)\| = \|A\| \leftrightarrow (1 \dots \|A\|) \approx A)$
11	7 10	mpbid	$⊢ A \in Fin \to (1 \dots \|A\|) \approx A$
12	1	derangen	$⊢ ((1 \dots \|A\|) \approx A \land A \in Fin) \to D ((1 \dots \|A\|)) = D (A)$
13	11 12	mpancom	$⊢ A \in Fin \to D ((1 \dots \|A\|)) = D (A)$
14	5 13	eqtr2d	$⊢ A \in Fin \to D (A) = S (\|A\|)$

Metamath Proof Explorer