Metamath Proof Explorer

Theorem derangsn

Description: The derangement number of a singleton. (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 derangsn ⊢ A ∈ V → D ⁡ A = 0

Proof

Step Hyp Ref Expression
1 derang.d ⊢ D = x ∈ Fin ⟼ f | f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y
2 snfi ⊢ A ∈ Fin
3 1 derangval ⊢ A ∈ Fin → D ⁡ A = f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y
4 2 3 ax-mp ⊢ D ⁡ A = f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y
5 f1of ⊢ f : A ⟶ 1-1 onto A → f : A ⟶ A
6 5 adantr ⊢ f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y → f : A ⟶ A
7 snidg ⊢ A ∈ V → A ∈ A
8 ffvelrn ⊢ f : A ⟶ A ∧ A ∈ A → f ⁡ A ∈ A
9 6 7 8 syl2anr ⊢ A ∈ V ∧ f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y → f ⁡ A ∈ A
10 simpr ⊢ f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y → ∀ y ∈ A f ⁡ y ≠ y
11 fveq2 ⊢ y = A → f ⁡ y = f ⁡ A
12 id ⊢ y = A → y = A
13 11 12 neeq12d ⊢ y = A → f ⁡ y ≠ y ↔ f ⁡ A ≠ A
14 13 rspcva ⊢ A ∈ A ∧ ∀ y ∈ A f ⁡ y ≠ y → f ⁡ A ≠ A
15 7 10 14 syl2an ⊢ A ∈ V ∧ f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y → f ⁡ A ≠ A
16 nelsn ⊢ f ⁡ A ≠ A → ¬ f ⁡ A ∈ A
17 15 16 syl ⊢ A ∈ V ∧ f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y → ¬ f ⁡ A ∈ A
18 9 17 pm2.21dd ⊢ A ∈ V ∧ f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y → f ∈ ∅
19 18 ex ⊢ A ∈ V → f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y → f ∈ ∅
20 19 abssdv ⊢ A ∈ V → f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y ⊆ ∅
21 ss0 ⊢ f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y ⊆ ∅ → f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y = ∅
22 20 21 syl ⊢ A ∈ V → f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y = ∅
23 22 fveq2d ⊢ A ∈ V → f | f : A ⟶ 1-1 onto A ∧ ∀ y ∈ A f ⁡ y ≠ y = ∅
24 4 23 eqtrid ⊢ A ∈ V → D ⁡ A = ∅
25 hash0 ⊢ ∅ = 0
26 24 25 eqtrdi ⊢ A ∈ V → D ⁡ A = 0