Metamath Proof Explorer


Theorem derangsn

Description: The derangement number of a singleton. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypothesis derang.d 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥1-1-onto𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
Assertion derangsn ( 𝐴𝑉 → ( 𝐷 ‘ { 𝐴 } ) = 0 )

Proof

Step Hyp Ref Expression
1 derang.d 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥1-1-onto𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
2 snfi { 𝐴 } ∈ Fin
3 1 derangval ( { 𝐴 } ∈ Fin → ( 𝐷 ‘ { 𝐴 } ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
4 2 3 ax-mp ( 𝐷 ‘ { 𝐴 } ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) } )
5 f1of ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } → 𝑓 : { 𝐴 } ⟶ { 𝐴 } )
6 5 adantr ( ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) → 𝑓 : { 𝐴 } ⟶ { 𝐴 } )
7 snidg ( 𝐴𝑉𝐴 ∈ { 𝐴 } )
8 ffvelrn ( ( 𝑓 : { 𝐴 } ⟶ { 𝐴 } ∧ 𝐴 ∈ { 𝐴 } ) → ( 𝑓𝐴 ) ∈ { 𝐴 } )
9 6 7 8 syl2anr ( ( 𝐴𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) ) → ( 𝑓𝐴 ) ∈ { 𝐴 } )
10 simpr ( ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) → ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 )
11 fveq2 ( 𝑦 = 𝐴 → ( 𝑓𝑦 ) = ( 𝑓𝐴 ) )
12 id ( 𝑦 = 𝐴𝑦 = 𝐴 )
13 11 12 neeq12d ( 𝑦 = 𝐴 → ( ( 𝑓𝑦 ) ≠ 𝑦 ↔ ( 𝑓𝐴 ) ≠ 𝐴 ) )
14 13 rspcva ( ( 𝐴 ∈ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) → ( 𝑓𝐴 ) ≠ 𝐴 )
15 7 10 14 syl2an ( ( 𝐴𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) ) → ( 𝑓𝐴 ) ≠ 𝐴 )
16 nelsn ( ( 𝑓𝐴 ) ≠ 𝐴 → ¬ ( 𝑓𝐴 ) ∈ { 𝐴 } )
17 15 16 syl ( ( 𝐴𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) ) → ¬ ( 𝑓𝐴 ) ∈ { 𝐴 } )
18 9 17 pm2.21dd ( ( 𝐴𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) ) → 𝑓 ∈ ∅ )
19 18 ex ( 𝐴𝑉 → ( ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) → 𝑓 ∈ ∅ ) )
20 19 abssdv ( 𝐴𝑉 → { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) } ⊆ ∅ )
21 ss0 ( { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) } ⊆ ∅ → { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) } = ∅ )
22 20 21 syl ( 𝐴𝑉 → { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) } = ∅ )
23 22 fveq2d ( 𝐴𝑉 → ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓𝑦 ) ≠ 𝑦 ) } ) = ( ♯ ‘ ∅ ) )
24 4 23 syl5eq ( 𝐴𝑉 → ( 𝐷 ‘ { 𝐴 } ) = ( ♯ ‘ ∅ ) )
25 hash0 ( ♯ ‘ ∅ ) = 0
26 24 25 eqtrdi ( 𝐴𝑉 → ( 𝐷 ‘ { 𝐴 } ) = 0 )