Metamath Proof Explorer


Theorem subfacp1

Description: A two-term recurrence for the subfactorial. This theorem allows us 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 syl5bb ( 𝑔 = 𝑓 → ( ∀ 𝑧 ∈ ( 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 ) ) ) ) )