Theorem subfacval

Description: The subfactorial is defined as the number of derangements (see derangval ) of the set ( 1 ... N ) . (Contributed by Mario Carneiro, 21-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2		subfac.n	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
4	3	fveq2d	⊢ ( 𝑛 = 𝑁 → ( 𝐷 ‘ ( 1 ... 𝑛 ) ) = ( 𝐷 ‘ ( 1 ... 𝑁 ) ) )
5		fvex	⊢ ( 𝐷 ‘ ( 1 ... 𝑁 ) ) ∈ V
6	4 2 5	fvmpt	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑆 ‘ 𝑁 ) = ( 𝐷 ‘ ( 1 ... 𝑁 ) ) )