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 ontox∧∀y∈xf⁡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 ontox∧∀y∈xf⁡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