Proof of Theorem subfaclefac
Step | Hyp | Ref
| Expression |
1 | | anidm 568 |
. . . . . 6
⊢ ((𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)) ↔ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)) |
2 | 1 | abbii 2803 |
. . . . 5
⊢ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁))} = {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} |
3 | | fzfid 13432 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ∈
Fin) |
4 | | deranglem 32699 |
. . . . . 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 2838 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin) |
7 | | simpl 486 |
. . . . 5
⊢ ((𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦) → 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)) |
8 | 7 | ss2abi 3956 |
. . . 4
⊢ {𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} |
9 | | ssdomg 8601 |
. . . 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 32699 |
. . . . 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 13832 |
. . . 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 587 |
. . 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 260 |
. 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 32706 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑆‘𝑁) = (𝐷‘(1...𝑁))) |
19 | 16 | derangval 32700 |
. . . 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 2773 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑆‘𝑁) = (♯‘{𝑓 ∣ (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ∧ ∀𝑦 ∈ (1...𝑁)(𝑓‘𝑦) ≠ 𝑦)})) |
22 | | hashfac 13910 |
. . . 4
⊢
((1...𝑁) ∈ Fin
→ (♯‘{𝑓
∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) = (!‘(♯‘(1...𝑁)))) |
23 | 3, 22 | syl 17 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (♯‘{𝑓
∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) = (!‘(♯‘(1...𝑁)))) |
24 | | hashfz1 13798 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) |
25 | 24 | fveq2d 6678 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (!‘(♯‘(1...𝑁))) = (!‘𝑁)) |
26 | 23, 25 | eqtr2d 2774 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) =
(♯‘{𝑓 ∣
𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
27 | 15, 21, 26 | 3brtr4d 5062 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑆‘𝑁) ≤ (!‘𝑁)) |