Metamath Proof Explorer

Theorem derang0

Description: The derangement number of the empty set. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypothesis derang.d ⊢D=x∈Fin⟼f|f:x⟶1-1 ontox∧∀y∈xf⁡y≠y
Assertion derang0 ⊢D⁡∅=1

Proof

Step Hyp Ref Expression
1 derang.d ⊢D=x∈Fin⟼f|f:x⟶1-1 ontox∧∀y∈xf⁡y≠y
2 0fin ⊢∅∈Fin
3 1 derangval ⊢∅∈Fin→D⁡∅=f|f:∅⟶1-1 onto∅∧∀y∈∅f⁡y≠y
4 2 3 ax-mp ⊢D⁡∅=f|f:∅⟶1-1 onto∅∧∀y∈∅f⁡y≠y
5 ral0 ⊢∀y∈∅f⁡y≠y
6 5 biantru ⊢f:∅⟶1-1 onto∅↔f:∅⟶1-1 onto∅∧∀y∈∅f⁡y≠y
7 eqid ⊢∅=∅
8 f1o00 ⊢f:∅⟶1-1 onto∅↔f=∅∧∅=∅
9 7 8 mpbiran2 ⊢f:∅⟶1-1 onto∅↔f=∅
10 6 9 bitr3i ⊢f:∅⟶1-1 onto∅∧∀y∈∅f⁡y≠y↔f=∅
11 10 abbii ⊢f|f:∅⟶1-1 onto∅∧∀y∈∅f⁡y≠y=f|f=∅
12 df-sn ⊢∅=f|f=∅
13 11 12 eqtr4i ⊢f|f:∅⟶1-1 onto∅∧∀y∈∅f⁡y≠y=∅
14 13 fveq2i ⊢f|f:∅⟶1-1 onto∅∧∀y∈∅f⁡y≠y=∅
15 0ex ⊢∅∈V
16 hashsng ⊢∅∈V→∅=1
17 15 16 ax-mp ⊢∅=1
18 4 14 17 3eqtri ⊢D⁡∅=1