Step | Hyp | Ref
| Expression |
1 | | f1eq2 6237 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:∅–1-1→𝐵)) |
2 | | f1fn 6242 |
. . . . . . . . . . . 12
⊢ (𝑓:∅–1-1→𝐵 → 𝑓 Fn ∅) |
3 | | fn0 6151 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn ∅ ↔ 𝑓 = ∅) |
4 | 2, 3 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝑓:∅–1-1→𝐵 → 𝑓 = ∅) |
5 | | f10 6310 |
. . . . . . . . . . . 12
⊢
∅:∅–1-1→𝐵 |
6 | | f1eq1 6236 |
. . . . . . . . . . . 12
⊢ (𝑓 = ∅ → (𝑓:∅–1-1→𝐵 ↔ ∅:∅–1-1→𝐵)) |
7 | 5, 6 | mpbiri 248 |
. . . . . . . . . . 11
⊢ (𝑓 = ∅ → 𝑓:∅–1-1→𝐵) |
8 | 4, 7 | impbii 199 |
. . . . . . . . . 10
⊢ (𝑓:∅–1-1→𝐵 ↔ 𝑓 = ∅) |
9 | | velsn 4332 |
. . . . . . . . . 10
⊢ (𝑓 ∈ {∅} ↔ 𝑓 = ∅) |
10 | 8, 9 | bitr4i 267 |
. . . . . . . . 9
⊢ (𝑓:∅–1-1→𝐵 ↔ 𝑓 ∈ {∅}) |
11 | 1, 10 | syl6bb 276 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓 ∈ {∅})) |
12 | 11 | abbi1dv 2892 |
. . . . . . 7
⊢ (𝑥 = ∅ → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {∅}) |
13 | 12 | fveq2d 6336 |
. . . . . 6
⊢ (𝑥 = ∅ →
(♯‘{𝑓 ∣
𝑓:𝑥–1-1→𝐵}) =
(♯‘{∅})) |
14 | | 0ex 4924 |
. . . . . . 7
⊢ ∅
∈ V |
15 | | hashsng 13361 |
. . . . . . 7
⊢ (∅
∈ V → (♯‘{∅}) = 1) |
16 | 14, 15 | ax-mp 5 |
. . . . . 6
⊢
(♯‘{∅}) = 1 |
17 | 13, 16 | syl6eq 2821 |
. . . . 5
⊢ (𝑥 = ∅ →
(♯‘{𝑓 ∣
𝑓:𝑥–1-1→𝐵}) = 1) |
18 | | fveq2 6332 |
. . . . . . . . 9
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
19 | | hash0 13360 |
. . . . . . . . 9
⊢
(♯‘∅) = 0 |
20 | 18, 19 | syl6eq 2821 |
. . . . . . . 8
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
0) |
21 | 20 | fveq2d 6336 |
. . . . . . 7
⊢ (𝑥 = ∅ →
(!‘(♯‘𝑥))
= (!‘0)) |
22 | | fac0 13267 |
. . . . . . 7
⊢
(!‘0) = 1 |
23 | 21, 22 | syl6eq 2821 |
. . . . . 6
⊢ (𝑥 = ∅ →
(!‘(♯‘𝑥))
= 1) |
24 | 20 | oveq2d 6809 |
. . . . . 6
⊢ (𝑥 = ∅ →
((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C0)) |
25 | 23, 24 | oveq12d 6811 |
. . . . 5
⊢ (𝑥 = ∅ →
((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = (1 · ((♯‘𝐵)C0))) |
26 | 17, 25 | eqeq12d 2786 |
. . . 4
⊢ (𝑥 = ∅ →
((♯‘{𝑓 ∣
𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) ↔ 1 = (1 ·
((♯‘𝐵)C0)))) |
27 | 26 | imbi2d 329 |
. . 3
⊢ (𝑥 = ∅ → ((𝐵 ∈ Fin →
(♯‘{𝑓 ∣
𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → 1 = (1 ·
((♯‘𝐵)C0))))) |
28 | | f1eq2 6237 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:𝑦–1-1→𝐵)) |
29 | 28 | abbidv 2890 |
. . . . . 6
⊢ (𝑥 = 𝑦 → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) |
30 | 29 | fveq2d 6336 |
. . . . 5
⊢ (𝑥 = 𝑦 → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})) |
31 | | fveq2 6332 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦)) |
32 | 31 | fveq2d 6336 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (!‘(♯‘𝑥)) =
(!‘(♯‘𝑦))) |
33 | 31 | oveq2d 6809 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝑦))) |
34 | 32, 33 | oveq12d 6811 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦)))) |
35 | 30, 34 | eqeq12d 2786 |
. . . 4
⊢ (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))))) |
36 | 35 | imbi2d 329 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦)))))) |
37 | | f1eq2 6237 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵)) |
38 | 37 | abbidv 2890 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) |
39 | 38 | fveq2d 6336 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵})) |
40 | | fveq2 6332 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧}))) |
41 | 40 | fveq2d 6336 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (!‘(♯‘𝑥)) =
(!‘(♯‘(𝑦
∪ {𝑧})))) |
42 | 40 | oveq2d 6809 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) |
43 | 41, 42 | oveq12d 6811 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))) |
44 | 39, 43 | eqeq12d 2786 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))) |
45 | 44 | imbi2d 329 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))) |
46 | | f1eq2 6237 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:𝐴–1-1→𝐵)) |
47 | 46 | abbidv 2890 |
. . . . . 6
⊢ (𝑥 = 𝐴 → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) |
48 | 47 | fveq2d 6336 |
. . . . 5
⊢ (𝑥 = 𝐴 → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) |
49 | | fveq2 6332 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴)) |
50 | 49 | fveq2d 6336 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (!‘(♯‘𝑥)) =
(!‘(♯‘𝐴))) |
51 | 49 | oveq2d 6809 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝐴))) |
52 | 50, 51 | oveq12d 6811 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝐴)) ·
((♯‘𝐵)C(♯‘𝐴)))) |
53 | 48, 52 | eqeq12d 2786 |
. . . 4
⊢ (𝑥 = 𝐴 → ((♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) ·
((♯‘𝐵)C(♯‘𝐴))))) |
54 | 53 | imbi2d 329 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) ·
((♯‘𝐵)C(♯‘𝐴)))))) |
55 | | hashcl 13349 |
. . . . . 6
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
56 | | bcn0 13301 |
. . . . . 6
⊢
((♯‘𝐵)
∈ ℕ0 → ((♯‘𝐵)C0) = 1) |
57 | 55, 56 | syl 17 |
. . . . 5
⊢ (𝐵 ∈ Fin →
((♯‘𝐵)C0) =
1) |
58 | 57 | oveq2d 6809 |
. . . 4
⊢ (𝐵 ∈ Fin → (1 ·
((♯‘𝐵)C0)) = (1
· 1)) |
59 | | 1t1e1 11377 |
. . . 4
⊢ (1
· 1) = 1 |
60 | 58, 59 | syl6req 2822 |
. . 3
⊢ (𝐵 ∈ Fin → 1 = (1
· ((♯‘𝐵)C0))) |
61 | | abn0 4101 |
. . . . . . . . . . . . 13
⊢ ({𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} ≠ ∅ ↔ ∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵) |
62 | | f1domg 8129 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ Fin → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵)) |
63 | 62 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵)) |
64 | | vex 3354 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑧 ∈ V |
65 | | hashunsng 13383 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))) |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
67 | 66 | adantl 467 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
68 | 67 | breq1d 4796 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵))) |
69 | | simprl 746 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin) |
70 | | snfi 8194 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑧} ∈ Fin |
71 | | unfi 8383 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
72 | 69, 70, 71 | sylancl 566 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin) |
73 | | simpl 468 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐵 ∈ Fin) |
74 | | hashdom 13370 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵)) |
75 | 72, 73, 74 | syl2anc 565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵)) |
76 | | hashcl 13349 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℕ0) |
77 | 76 | ad2antrl 699 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝑦) ∈
ℕ0) |
78 | | nn0p1nn 11534 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑦)
∈ ℕ0 → ((♯‘𝑦) + 1) ∈ ℕ) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝑦) + 1) ∈ ℕ) |
80 | 79 | nnred 11237 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝑦) + 1) ∈ ℝ) |
81 | 55 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝐵) ∈
ℕ0) |
82 | 81 | nn0red 11554 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝐵) ∈ ℝ) |
83 | 80, 82 | lenltd 10385 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (((♯‘𝑦) + 1) ≤ (♯‘𝐵) ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1))) |
84 | 68, 75, 83 | 3bitr3d 298 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝑦 ∪ {𝑧}) ≼ 𝐵 ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1))) |
85 | 63, 84 | sylibd 229 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1))) |
86 | 85 | exlimdv 2013 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1))) |
87 | 61, 86 | syl5bi 232 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ({𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} ≠ ∅ → ¬
(♯‘𝐵) <
((♯‘𝑦) +
1))) |
88 | 87 | necon4ad 2962 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝐵) < ((♯‘𝑦) + 1) → {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} = ∅)) |
89 | 88 | imp 393 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} = ∅) |
90 | 89 | fveq2d 6336 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) =
(♯‘∅)) |
91 | | hashcl 13349 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∪ {𝑧}) ∈ Fin → (♯‘(𝑦 ∪ {𝑧})) ∈
ℕ0) |
92 | 72, 91 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝑦 ∪ {𝑧})) ∈
ℕ0) |
93 | | faccl 13274 |
. . . . . . . . . . . . 13
⊢
((♯‘(𝑦
∪ {𝑧})) ∈
ℕ0 → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ) |
95 | 94 | nncnd 11238 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ) |
96 | 95 | adantr 466 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ) |
97 | 96 | mul01d 10437 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) →
((!‘(♯‘(𝑦
∪ {𝑧}))) · 0) =
0) |
98 | 19, 90, 97 | 3eqtr4a 2831 |
. . . . . . . 8
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0)) |
99 | 67 | adantr 466 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
100 | 99 | oveq2d 6809 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1))) |
101 | 81 | adantr 466 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) ∈
ℕ0) |
102 | 79 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈
ℕ) |
103 | 102 | nnzd 11683 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈
ℤ) |
104 | | simpr 471 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) < ((♯‘𝑦) + 1)) |
105 | 104 | olcd 853 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (((♯‘𝑦) + 1) < 0 ∨
(♯‘𝐵) <
((♯‘𝑦) +
1))) |
106 | | bcval4 13298 |
. . . . . . . . . . 11
⊢
(((♯‘𝐵)
∈ ℕ0 ∧ ((♯‘𝑦) + 1) ∈ ℤ ∧
(((♯‘𝑦) + 1)
< 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1))) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0) |
107 | 101, 103,
105, 106 | syl3anc 1476 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0) |
108 | 100, 107 | eqtrd 2805 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = 0) |
109 | 108 | oveq2d 6809 |
. . . . . . . 8
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) →
((!‘(♯‘(𝑦
∪ {𝑧}))) ·
((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0)) |
110 | 98, 109 | eqtr4d 2808 |
. . . . . . 7
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))) |
111 | 110 | a1d 25 |
. . . . . 6
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))) |
112 | | oveq2 6801 |
. . . . . . 7
⊢
((♯‘{𝑓
∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) → (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))))) |
113 | 69 | adantr 466 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝑦 ∈ Fin) |
114 | 73 | adantr 466 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝐵 ∈ Fin) |
115 | | simplrr 755 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ¬ 𝑧 ∈ 𝑦) |
116 | | simpr 471 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) |
117 | 113, 114,
115, 116 | hashf1lem2 13442 |
. . . . . . . 8
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}))) |
118 | 81 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈
ℕ0) |
119 | | faccl 13274 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐵)
∈ ℕ0 → (!‘(♯‘𝐵)) ∈ ℕ) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈
ℕ) |
121 | 120 | nncnd 11238 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈
ℂ) |
122 | 77 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈
ℕ0) |
123 | | peano2nn0 11535 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑦)
∈ ℕ0 → ((♯‘𝑦) + 1) ∈
ℕ0) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈
ℕ0) |
125 | | nn0sub2 11640 |
. . . . . . . . . . . . . . 15
⊢
((((♯‘𝑦)
+ 1) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
((♯‘𝑦) + 1)
≤ (♯‘𝐵))
→ ((♯‘𝐵)
− ((♯‘𝑦)
+ 1)) ∈ ℕ0) |
126 | 124, 118,
116, 125 | syl3anc 1476 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈
ℕ0) |
127 | | faccl 13274 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐵)
− ((♯‘𝑦)
+ 1)) ∈ ℕ0 → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈
ℕ) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈
ℕ) |
129 | 128 | nncnd 11238 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈
ℂ) |
130 | 128 | nnne0d 11267 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ≠
0) |
131 | 121, 129,
130 | divcld 11003 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) ∈ ℂ) |
132 | | faccl 13274 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝑦)
+ 1) ∈ ℕ0 → (!‘((♯‘𝑦) + 1)) ∈
ℕ) |
133 | 124, 132 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈
ℕ) |
134 | 133 | nncnd 11238 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈
ℂ) |
135 | 133 | nnne0d 11267 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ≠ 0) |
136 | 131, 134,
135 | divcan2d 11005 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) /
(!‘((♯‘𝑦)
+ 1)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))))) |
137 | 118 | nn0cnd 11555 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ) |
138 | 122 | nn0cnd 11555 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℂ) |
139 | 137, 138 | subcld 10594 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ) |
140 | | ax-1cn 10196 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
141 | | npcan 10492 |
. . . . . . . . . . . . . 14
⊢
((((♯‘𝐵)
− (♯‘𝑦))
∈ ℂ ∧ 1 ∈ ℂ) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) =
((♯‘𝐵) −
(♯‘𝑦))) |
142 | 139, 140,
141 | sylancl 566 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) =
((♯‘𝐵) −
(♯‘𝑦))) |
143 | | 1cnd 10258 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 1 ∈ ℂ) |
144 | 137, 138,
143 | subsub4d 10625 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) = ((♯‘𝐵) − ((♯‘𝑦) + 1))) |
145 | 144, 126 | eqeltrd 2850 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) ∈
ℕ0) |
146 | | nn0p1nn 11534 |
. . . . . . . . . . . . . 14
⊢
((((♯‘𝐵)
− (♯‘𝑦))
− 1) ∈ ℕ0 → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈
ℕ) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈
ℕ) |
148 | 142, 147 | eqeltrrd 2851 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ) |
149 | 148 | nnne0d 11267 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ≠ 0) |
150 | 131, 139,
149 | divcan2d 11005 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1))))) |
151 | 136, 150 | eqtr4d 2808 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) /
(!‘((♯‘𝑦)
+ 1)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦))))) |
152 | 67 | adantr 466 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
153 | 152 | fveq2d 6336 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) = (!‘((♯‘𝑦) + 1))) |
154 | | nn0uz 11924 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
155 | 124, 154 | syl6eleq 2860 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈
(ℤ≥‘0)) |
156 | 118 | nn0zd 11682 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ) |
157 | | elfz5 12541 |
. . . . . . . . . . . . . 14
⊢
((((♯‘𝑦)
+ 1) ∈ (ℤ≥‘0) ∧ (♯‘𝐵) ∈ ℤ) →
(((♯‘𝑦) + 1)
∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵))) |
158 | 155, 156,
157 | syl2anc 565 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝑦) + 1) ∈
(0...(♯‘𝐵))
↔ ((♯‘𝑦) +
1) ≤ (♯‘𝐵))) |
159 | 116, 158 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵))) |
160 | | bcval2 13296 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑦)
+ 1) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ·
(!‘((♯‘𝑦)
+ 1))))) |
161 | 159, 160 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ·
(!‘((♯‘𝑦)
+ 1))))) |
162 | 152 | oveq2d 6809 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1))) |
163 | 121, 129,
134, 130, 135 | divdiv1d 11034 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / (!‘((♯‘𝑦) + 1))) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ·
(!‘((♯‘𝑦)
+ 1))))) |
164 | 161, 162,
163 | 3eqtr4d 2815 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / (!‘((♯‘𝑦) + 1)))) |
165 | 153, 164 | oveq12d 6811 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘((♯‘𝑦) + 1)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) /
(!‘((♯‘𝑦)
+ 1))))) |
166 | 122, 154 | syl6eleq 2860 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈
(ℤ≥‘0)) |
167 | | peano2fzr 12561 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝑦)
∈ (ℤ≥‘0) ∧ ((♯‘𝑦) + 1) ∈
(0...(♯‘𝐵)))
→ (♯‘𝑦)
∈ (0...(♯‘𝐵))) |
168 | 166, 159,
167 | syl2anc 565 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (0...(♯‘𝐵))) |
169 | | bcval2 13296 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑦)
∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦))))) |
170 | 168, 169 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦))))) |
171 | | elfzle2 12552 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑦)
∈ (0...(♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵)) |
172 | 168, 171 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵)) |
173 | | nn0sub2 11640 |
. . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝑦)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
(♯‘𝑦) ≤
(♯‘𝐵)) →
((♯‘𝐵) −
(♯‘𝑦)) ∈
ℕ0) |
174 | 122, 118,
172, 173 | syl3anc 1476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈
ℕ0) |
175 | | faccl 13274 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘𝐵)
− (♯‘𝑦))
∈ ℕ0 → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℕ) |
176 | 174, 175 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈
ℕ) |
177 | 176 | nncnd 11238 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈
ℂ) |
178 | | faccl 13274 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑦)
∈ ℕ0 → (!‘(♯‘𝑦)) ∈ ℕ) |
179 | 122, 178 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈
ℕ) |
180 | 179 | nncnd 11238 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈
ℂ) |
181 | 176 | nnne0d 11267 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ≠ 0) |
182 | 179 | nnne0d 11267 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ≠ 0) |
183 | 121, 177,
180, 181, 182 | divdiv1d 11034 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− (♯‘𝑦)))) / (!‘(♯‘𝑦))) =
((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) ·
(!‘(♯‘𝑦))))) |
184 | 170, 183 | eqtr4d 2808 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− (♯‘𝑦)))) / (!‘(♯‘𝑦)))) |
185 | 184 | oveq2d 6809 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) = ((!‘(♯‘𝑦)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) /
(!‘(♯‘𝑦))))) |
186 | | facnn2 13273 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝐵)
− (♯‘𝑦))
∈ ℕ → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) ·
((♯‘𝐵) −
(♯‘𝑦)))) |
187 | 148, 186 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) =
((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦)))) |
188 | 144 | fveq2d 6336 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) =
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) |
189 | 188 | oveq1d 6808 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) ·
((♯‘𝐵) −
(♯‘𝑦))) =
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))) |
190 | 187, 189 | eqtrd 2805 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) =
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))) |
191 | 190 | oveq2d 6809 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− (♯‘𝑦)))) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))) |
192 | 121, 177,
181 | divcld 11003 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− (♯‘𝑦)))) ∈ ℂ) |
193 | 192, 180,
182 | divcan2d 11005 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) /
(!‘(♯‘𝑦)))) = ((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− (♯‘𝑦))))) |
194 | 121, 129,
139, 130, 149 | divdiv1d 11034 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦))) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))) |
195 | 191, 193,
194 | 3eqtr4d 2815 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) /
(!‘(♯‘𝑦)))) = (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) |
196 | 185, 195 | eqtrd 2805 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) = (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) |
197 | 196 | oveq2d 6809 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦))))) |
198 | 151, 165,
197 | 3eqtr4d 2815 |
. . . . . . . 8
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))))) |
199 | 117, 198 | eqeq12d 2786 |
. . . . . . 7
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) ↔ (((♯‘𝐵) − (♯‘𝑦)) ·
(♯‘{𝑓 ∣
𝑓:𝑦–1-1→𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦)))))) |
200 | 112, 199 | syl5ibr 236 |
. . . . . 6
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))) |
201 | 111, 200,
82, 80 | ltlecasei 10347 |
. . . . 5
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))) |
202 | 201 | expcom 398 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝐵 ∈ Fin → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))) |
203 | 202 | a2d 29 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦)))) → (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))) |
204 | 27, 36, 45, 54, 60, 203 | findcard2s 8357 |
. 2
⊢ (𝐴 ∈ Fin → (𝐵 ∈ Fin →
(♯‘{𝑓 ∣
𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) ·
((♯‘𝐵)C(♯‘𝐴))))) |
205 | 204 | imp 393 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘{𝑓 ∣
𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) ·
((♯‘𝐵)C(♯‘𝐴)))) |