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 ∈ Fin ⟼ f | f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y
Assertion derangval ⊢ A ∈ Fin → D ⁡ A = f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y

Proof

Step Hyp Ref Expression
1 derang.d ⊢ D = x ∈ Fin ⟼ f | f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y
2 f1oeq2 ⊢ x = A → f : x ⟶ 1-1 onto x ↔ f : A ⟶ 1-1 onto x
3 f1oeq3 ⊢ x = A → f : A ⟶ 1-1 onto x ↔ f : A ⟶ 1-1 onto A
4 2 3 bitrd ⊢ x = A → f : x ⟶ 1-1 onto x ↔ f : A ⟶ 1-1 onto A
5 raleq ⊢ x = A → ∀ y ∈ x f ⁡ y ≠ y ↔ ∀ y ∈ A f ⁡ y ≠ y
6 4 5 anbi12d ⊢ x = A → f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y ↔ f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y
7 6 abbidv ⊢ x = A → f | f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y = f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y
8 7 fveq2d ⊢ x = A → f | f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y = f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y
9 fvex ⊢ f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y ∈ V
10 8 1 9 fvmpt ⊢ A ∈ Fin → D ⁡ A = f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y