Metamath Proof Explorer

Theorem derangen

Description: The derangement number is a cardinal invariant, i.e. it only depends on the size of a set and not on its contents. (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypothesis derang.d ⊢ D = x ∈ Fin ⟼ f | f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y
Assertion derangen ⊢ A ≈ B ∧ B ∈ Fin → D ⁡ A = D ⁡ B

Proof

Step Hyp Ref Expression
1 derang.d ⊢ D = x ∈ Fin ⟼ f | f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y
2 1 derangenlem ⊢ A ≈ B ∧ B ∈ Fin → D ⁡ A ≤ D ⁡ B
3 ensym ⊢ A ≈ B → B ≈ A
4 3 adantr ⊢ A ≈ B ∧ B ∈ Fin → B ≈ A
5 enfi ⊢ A ≈ B → A ∈ Fin ↔ B ∈ Fin
6 5 biimpar ⊢ A ≈ B ∧ B ∈ Fin → A ∈ Fin
7 1 derangenlem ⊢ B ≈ A ∧ A ∈ Fin → D ⁡ B ≤ D ⁡ A
8 4 6 7 syl2anc ⊢ A ≈ B ∧ B ∈ Fin → D ⁡ B ≤ D ⁡ A
9 1 derangf ⊢ D : Fin ⟶ ℕ 0
10 9 ffvelcdmi ⊢ A ∈ Fin → D ⁡ A ∈ ℕ 0
11 6 10 syl ⊢ A ≈ B ∧ B ∈ Fin → D ⁡ A ∈ ℕ 0
12 9 ffvelcdmi ⊢ B ∈ Fin → D ⁡ B ∈ ℕ 0
13 12 adantl ⊢ A ≈ B ∧ B ∈ Fin → D ⁡ B ∈ ℕ 0
14 nn0re ⊢ D ⁡ A ∈ ℕ 0 → D ⁡ A ∈ ℝ
15 nn0re ⊢ D ⁡ B ∈ ℕ 0 → D ⁡ B ∈ ℝ
16 letri3 ⊢ D ⁡ A ∈ ℝ ∧ D ⁡ B ∈ ℝ → D ⁡ A = D ⁡ B ↔ D ⁡ A ≤ D ⁡ B ∧ D ⁡ B ≤ D ⁡ A
17 14 15 16 syl2an ⊢ D ⁡ A ∈ ℕ 0 ∧ D ⁡ B ∈ ℕ 0 → D ⁡ A = D ⁡ B ↔ D ⁡ A ≤ D ⁡ B ∧ D ⁡ B ≤ D ⁡ A
18 11 13 17 syl2anc ⊢ A ≈ B ∧ B ∈ Fin → D ⁡ A = D ⁡ B ↔ D ⁡ A ≤ D ⁡ B ∧ D ⁡ B ≤ D ⁡ A
19 2 8 18 mpbir2and ⊢ A ≈ B ∧ B ∈ Fin → D ⁡ A = D ⁡ B