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 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y
Assertion derang0 ⊢ D ⁡ ∅ = 1

Proof

Step Hyp Ref Expression
1 derang.d ⊢ D = x ∈ Fin ⟼ f | f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ 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