Theorem subfacp1

Description: A two-term recurrence for the subfactorial. This theorem allows to forget the combinatorial definition of the derangement number in favor of the recursive definition provided by this theorem and subfac0 , subfac1 . (Contributed by Mario Carneiro, 23-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		derang.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2		subfac.n	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3		f1oeq1	⊢ ( 𝑔 = 𝑓 → ( 𝑔 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ↔ 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
4		fveq2	⊢ ( 𝑧 = 𝑦 → ( 𝑔 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑦 ) )
5		id	⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
6	4 5	neeq12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑔 ‘ 𝑧 ) ≠ 𝑧 ↔ ( 𝑔 ‘ 𝑦 ) ≠ 𝑦 ) )
7	6	cbvralvw	⊢ ( ∀ 𝑧 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑔 ‘ 𝑧 ) ≠ 𝑧 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑔 ‘ 𝑦 ) ≠ 𝑦 )
8		fveq1	⊢ ( 𝑔 = 𝑓 → ( 𝑔 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
9	8	neeq1d	⊢ ( 𝑔 = 𝑓 → ( ( 𝑔 ‘ 𝑦 ) ≠ 𝑦 ↔ ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) )
10	9	ralbidv	⊢ ( 𝑔 = 𝑓 → ( ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑔 ‘ 𝑦 ) ≠ 𝑦 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) )
11	7 10	bitrid	⊢ ( 𝑔 = 𝑓 → ( ∀ 𝑧 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑔 ‘ 𝑧 ) ≠ 𝑧 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) )
12	3 11	anbi12d	⊢ ( 𝑔 = 𝑓 → ( ( 𝑔 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑧 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑔 ‘ 𝑧 ) ≠ 𝑧 ) ↔ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ) )
13	12	cbvabv	⊢ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑧 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑔 ‘ 𝑧 ) ≠ 𝑧 ) } = { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) }
14	1 2 13	subfacp1lem6	⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ‘ ( 𝑁 + 1 ) ) = ( 𝑁 · ( ( 𝑆 ‘ 𝑁 ) + ( 𝑆 ‘ ( 𝑁 − 1 ) ) ) ) )