Step |
Hyp |
Ref |
Expression |
1 |
|
derang.d |
⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) ) |
2 |
|
subfac.n |
⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) ) |
3 |
|
hashcl |
⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) |
4 |
1 2
|
subfacval |
⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( 𝑆 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐷 ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) |
5 |
3 4
|
syl |
⊢ ( 𝐴 ∈ Fin → ( 𝑆 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐷 ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) |
6 |
|
hashfz1 |
⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) ) |
7 |
3 6
|
syl |
⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) ) |
8 |
|
fzfid |
⊢ ( 𝐴 ∈ Fin → ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin ) |
9 |
|
hashen |
⊢ ( ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ) ) |
10 |
8 9
|
mpancom |
⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ 𝐴 ) ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ) ) |
11 |
7 10
|
mpbid |
⊢ ( 𝐴 ∈ Fin → ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ) |
12 |
1
|
derangen |
⊢ ( ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐷 ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( 𝐷 ‘ 𝐴 ) ) |
13 |
11 12
|
mpancom |
⊢ ( 𝐴 ∈ Fin → ( 𝐷 ‘ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) = ( 𝐷 ‘ 𝐴 ) ) |
14 |
5 13
|
eqtr2d |
⊢ ( 𝐴 ∈ Fin → ( 𝐷 ‘ 𝐴 ) = ( 𝑆 ‘ ( ♯ ‘ 𝐴 ) ) ) |