Theorem subfac0

Description: The subfactorial at zero. (Contributed by Mario Carneiro, 19-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2		subfac.n	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3		0nn0	⊢ 0 ∈ ℕ0
4	1 2	subfacval	⊢ ( 0 ∈ ℕ0 → ( 𝑆 ‘ 0 ) = ( 𝐷 ‘ ( 1 ... 0 ) ) )
5	3 4	ax-mp	⊢ ( 𝑆 ‘ 0 ) = ( 𝐷 ‘ ( 1 ... 0 ) )
6		fz10	⊢ ( 1 ... 0 ) = ∅
7	6	fveq2i	⊢ ( 𝐷 ‘ ( 1 ... 0 ) ) = ( 𝐷 ‘ ∅ )
8	1	derang0	⊢ ( 𝐷 ‘ ∅ ) = 1
9	5 7 8	3eqtri	⊢ ( 𝑆 ‘ 0 ) = 1