Metamath Proof Explorer


Theorem derangen2

Description: Write the derangement number in terms of the subfactorial. (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses derang.d 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥1-1-onto𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
subfac.n 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
Assertion derangen2 ( 𝐴 ∈ Fin → ( 𝐷𝐴 ) = ( 𝑆 ‘ ( ♯ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 derang.d 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥1-1-onto𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
2 subfac.n 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3 hashcl ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
4 1 2 subfacval ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( 𝑆 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐷 ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
5 3 4 syl ( 𝐴 ∈ Fin → ( 𝑆 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐷 ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
6 hashfz1 ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) )
7 3 6 syl ( 𝐴 ∈ Fin → ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) )
8 fzfid ( 𝐴 ∈ Fin → ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin )
9 hashen ( ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ) )
10 8 9 mpancom ( 𝐴 ∈ Fin → ( ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ) )
11 7 10 mpbid ( 𝐴 ∈ Fin → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )
12 1 derangen ( ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴𝐴 ∈ Fin ) → ( 𝐷 ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( 𝐷𝐴 ) )
13 11 12 mpancom ( 𝐴 ∈ Fin → ( 𝐷 ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( 𝐷𝐴 ) )
14 5 13 eqtr2d ( 𝐴 ∈ Fin → ( 𝐷𝐴 ) = ( 𝑆 ‘ ( ♯ ‘ 𝐴 ) ) )