Theorem subfacf

Description: The subfactorial is a function from nonnegative integers to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2		subfac.n	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3		fzfi	⊢ ( 1 ... 𝑛 ) ∈ Fin
4	1	derangf	⊢ 𝐷 : Fin ⟶ ℕ0
5	4	ffvelcdmi	⊢ ( ( 1 ... 𝑛 ) ∈ Fin → ( 𝐷 ‘ ( 1 ... 𝑛 ) ) ∈ ℕ0 )
6	3 5	ax-mp	⊢ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) ∈ ℕ0
7	6	rgenw	⊢ ∀ 𝑛 ∈ ℕ0 ( 𝐷 ‘ ( 1 ... 𝑛 ) ) ∈ ℕ0
8	2	fmpt	⊢ ( ∀ 𝑛 ∈ ℕ0 ( 𝐷 ‘ ( 1 ... 𝑛 ) ) ∈ ℕ0 ↔ 𝑆 : ℕ0 ⟶ ℕ0 )
9	7 8	mpbi	⊢ 𝑆 : ℕ0 ⟶ ℕ0