Metamath Proof Explorer

Theorem derangval

Description: Define the derangement function, which counts the number of bijections from a set to itself such that no element is mapped to itself. (Contributed by Mario Carneiro, 19-Jan-2015)

		Ref	Expression
	Hypothesis	derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
	Assertion	derangval	$⊢ A \in Fin \to D (A) = \|\{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}\|$

Proof

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		f1oeq2	$⊢ x = A \to (f : x \underset{1-1 onto}{⟶} x \leftrightarrow f : A \underset{1-1 onto}{⟶} x)$
3		f1oeq3	$⊢ x = A \to (f : A \underset{1-1 onto}{⟶} x \leftrightarrow f : A \underset{1-1 onto}{⟶} A)$
4	2 3	bitrd	$⊢ x = A \to (f : x \underset{1-1 onto}{⟶} x \leftrightarrow f : A \underset{1-1 onto}{⟶} A)$
5		raleq	$⊢ x = A \to (\forall y \in x f (y) \neq y \leftrightarrow \forall y \in A f (y) \neq y)$
6	4 5	anbi12d	$⊢ x = A \to ((f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y) \leftrightarrow (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y))$
7	6	abbidv	$⊢ x = A \to \{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\} = \{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}$
8	7	fveq2d	$⊢ x = A \to \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\| = \|\{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}\|$
9		fvex	$⊢ \|\{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}\| \in V$
10	8 1 9	fvmpt	$⊢ A \in Fin \to D (A) = \|\{f \| (f : A \underset{1-1 onto}{⟶} A \land \forall y \in A f (y) \neq y)\}\|$