Proof of Theorem subfaclefac
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | anidm 564 | . . . . . 6
⊢ ((𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)) ↔ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 2 | 1 | abbii 2808 | . . . . 5
⊢ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁))} = {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} | 
| 3 |  | fzfid 14015 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ∈
Fin) | 
| 4 |  | deranglem 35172 | . . . . . 6
⊢
((1...𝑁) ∈ Fin
→ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁))} ∈ Fin) | 
| 5 | 3, 4 | syl 17 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁))} ∈ Fin) | 
| 6 | 2, 5 | eqeltrrid 2845 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin) | 
| 7 |  | simpl 482 | . . . . 5
⊢ ((𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦) → 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)) | 
| 8 | 7 | ss2abi 4066 | . . . 4
⊢ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} | 
| 9 |  | ssdomg 9041 | . . . 4
⊢ ({𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin → ({𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} → {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) | 
| 10 | 6, 8, 9 | mpisyl 21 | . . 3
⊢ (𝑁 ∈ ℕ0
→ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) | 
| 11 |  | deranglem 35172 | . . . . 5
⊢
((1...𝑁) ∈ Fin
→ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin) | 
| 12 | 3, 11 | syl 17 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin) | 
| 13 |  | hashdom 14419 | . . . 4
⊢ (({𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)} ∈ Fin ∧ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin) → ((♯‘{𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ↔ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) | 
| 14 | 12, 6, 13 | syl2anc 584 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ((♯‘{𝑓
∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ↔ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)} ≼ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) | 
| 15 | 10, 14 | mpbird 257 | . 2
⊢ (𝑁 ∈ ℕ0
→ (♯‘{𝑓
∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)}) ≤ (♯‘{𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) | 
| 16 |  | derang.d | . . . 4
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)})) | 
| 17 |  | subfac.n | . . . 4
⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛))) | 
| 18 | 16, 17 | subfacval 35179 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑆‘𝑁) = (𝐷‘(1...𝑁))) | 
| 19 | 16 | derangval 35173 | . . . 4
⊢
((1...𝑁) ∈ Fin
→ (𝐷‘(1...𝑁)) = (♯‘{𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)})) | 
| 20 | 3, 19 | syl 17 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐷‘(1...𝑁)) = (♯‘{𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)})) | 
| 21 | 18, 20 | eqtrd 2776 | . 2
⊢ (𝑁 ∈ ℕ0
→ (𝑆‘𝑁) = (♯‘{𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)})) | 
| 22 |  | hashfac 14498 | . . . 4
⊢
((1...𝑁) ∈ Fin
→ (♯‘{𝑓
∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) = (!‘(♯‘(1...𝑁)))) | 
| 23 | 3, 22 | syl 17 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (♯‘{𝑓
∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) = (!‘(♯‘(1...𝑁)))) | 
| 24 |  | hashfz1 14386 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) | 
| 25 | 24 | fveq2d 6909 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (!‘(♯‘(1...𝑁))) = (!‘𝑁)) | 
| 26 | 23, 25 | eqtr2d 2777 | . 2
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) =
(♯‘{𝑓 ∣
𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) | 
| 27 | 15, 21, 26 | 3brtr4d 5174 | 1
⊢ (𝑁 ∈ ℕ0
→ (𝑆‘𝑁) ≤ (!‘𝑁)) |