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 → ( 𝐷 ‘ 𝐴 ) = ( 𝑆 ‘ ( ♯ ‘ 𝐴 ) ) )