Theorem subfac1

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

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

Proof

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