Step | Hyp | Ref
| Expression |
1 | | f1eq2 6571 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:∅–1-1→𝐵)) |
2 | | f1fn 6576 |
. . . . . . . . . . . 12
⊢ (𝑓:∅–1-1→𝐵 → 𝑓 Fn ∅) |
3 | | fn0 6469 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn ∅ ↔ 𝑓 = ∅) |
4 | 2, 3 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝑓:∅–1-1→𝐵 → 𝑓 = ∅) |
5 | | f10 6651 |
. . . . . . . . . . . 12
⊢
∅:∅–1-1→𝐵 |
6 | | f1eq1 6570 |
. . . . . . . . . . . 12
⊢ (𝑓 = ∅ → (𝑓:∅–1-1→𝐵 ↔ ∅:∅–1-1→𝐵)) |
7 | 5, 6 | mpbiri 261 |
. . . . . . . . . . 11
⊢ (𝑓 = ∅ → 𝑓:∅–1-1→𝐵) |
8 | 4, 7 | impbii 212 |
. . . . . . . . . 10
⊢ (𝑓:∅–1-1→𝐵 ↔ 𝑓 = ∅) |
9 | | velsn 4533 |
. . . . . . . . . 10
⊢ (𝑓 ∈ {∅} ↔ 𝑓 = ∅) |
10 | 8, 9 | bitr4i 281 |
. . . . . . . . 9
⊢ (𝑓:∅–1-1→𝐵 ↔ 𝑓 ∈ {∅}) |
11 | 1, 10 | bitrdi 290 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓 ∈ {∅})) |
12 | 11 | abbi1dv 2870 |
. . . . . . 7
⊢ (𝑥 = ∅ → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {∅}) |
13 | 12 | fveq2d 6679 |
. . . . . 6
⊢ (𝑥 = ∅ →
(♯‘{𝑓 ∣
𝑓:𝑥–1-1→𝐵}) =
(♯‘{∅})) |
14 | | 0ex 5176 |
. . . . . . 7
⊢ ∅
∈ V |
15 | | hashsng 13823 |
. . . . . . 7
⊢ (∅
∈ V → (♯‘{∅}) = 1) |
16 | 14, 15 | ax-mp 5 |
. . . . . 6
⊢
(♯‘{∅}) = 1 |
17 | 13, 16 | eqtrdi 2789 |
. . . . 5
⊢ (𝑥 = ∅ →
(♯‘{𝑓 ∣
𝑓:𝑥–1-1→𝐵}) = 1) |
18 | | fveq2 6675 |
. . . . . . . . 9
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
19 | | hash0 13821 |
. . . . . . . . 9
⊢
(♯‘∅) = 0 |
20 | 18, 19 | eqtrdi 2789 |
. . . . . . . 8
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
0) |
21 | 20 | fveq2d 6679 |
. . . . . . 7
⊢ (𝑥 = ∅ →
(!‘(♯‘𝑥))
= (!‘0)) |
22 | | fac0 13729 |
. . . . . . 7
⊢
(!‘0) = 1 |
23 | 21, 22 | eqtrdi 2789 |
. . . . . 6
⊢ (𝑥 = ∅ →
(!‘(♯‘𝑥))
= 1) |
24 | 20 | oveq2d 7187 |
. . . . . 6
⊢ (𝑥 = ∅ →
((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C0)) |
25 | 23, 24 | oveq12d 7189 |
. . . . 5
⊢ (𝑥 = ∅ →
((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = (1 · ((♯‘𝐵)C0))) |
26 | 17, 25 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = ∅ →
((♯‘{𝑓 ∣
𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) ↔ 1 = (1 ·
((♯‘𝐵)C0)))) |
27 | 26 | imbi2d 344 |
. . 3
⊢ (𝑥 = ∅ → ((𝐵 ∈ Fin →
(♯‘{𝑓 ∣
𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → 1 = (1 ·
((♯‘𝐵)C0))))) |
28 | | f1eq2 6571 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:𝑦–1-1→𝐵)) |
29 | 28 | abbidv 2802 |
. . . . . 6
⊢ (𝑥 = 𝑦 → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) |
30 | 29 | fveq2d 6679 |
. . . . 5
⊢ (𝑥 = 𝑦 → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})) |
31 | | 2fveq3 6680 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (!‘(♯‘𝑥)) =
(!‘(♯‘𝑦))) |
32 | | fveq2 6675 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦)) |
33 | 32 | oveq2d 7187 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝑦))) |
34 | 31, 33 | oveq12d 7189 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦)))) |
35 | 30, 34 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))))) |
36 | 35 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦)))))) |
37 | | f1eq2 6571 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵)) |
38 | 37 | abbidv 2802 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) |
39 | 38 | fveq2d 6679 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵})) |
40 | | 2fveq3 6680 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (!‘(♯‘𝑥)) =
(!‘(♯‘(𝑦
∪ {𝑧})))) |
41 | | fveq2 6675 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧}))) |
42 | 41 | oveq2d 7187 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) |
43 | 40, 42 | oveq12d 7189 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))) |
44 | 39, 43 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))) |
45 | 44 | imbi2d 344 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))) |
46 | | f1eq2 6571 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:𝐴–1-1→𝐵)) |
47 | 46 | abbidv 2802 |
. . . . . 6
⊢ (𝑥 = 𝐴 → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) |
48 | 47 | fveq2d 6679 |
. . . . 5
⊢ (𝑥 = 𝐴 → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) |
49 | | 2fveq3 6680 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (!‘(♯‘𝑥)) =
(!‘(♯‘𝐴))) |
50 | | fveq2 6675 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴)) |
51 | 50 | oveq2d 7187 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝐴))) |
52 | 49, 51 | oveq12d 7189 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝐴)) ·
((♯‘𝐵)C(♯‘𝐴)))) |
53 | 48, 52 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = 𝐴 → ((♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) ·
((♯‘𝐵)C(♯‘𝐴))))) |
54 | 53 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) ·
((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) ·
((♯‘𝐵)C(♯‘𝐴)))))) |
55 | | hashcl 13810 |
. . . . . 6
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
56 | | bcn0 13763 |
. . . . . 6
⊢
((♯‘𝐵)
∈ ℕ0 → ((♯‘𝐵)C0) = 1) |
57 | 55, 56 | syl 17 |
. . . . 5
⊢ (𝐵 ∈ Fin →
((♯‘𝐵)C0) =
1) |
58 | 57 | oveq2d 7187 |
. . . 4
⊢ (𝐵 ∈ Fin → (1 ·
((♯‘𝐵)C0)) = (1
· 1)) |
59 | | 1t1e1 11879 |
. . . 4
⊢ (1
· 1) = 1 |
60 | 58, 59 | eqtr2di 2790 |
. . 3
⊢ (𝐵 ∈ Fin → 1 = (1
· ((♯‘𝐵)C0))) |
61 | | abn0 4270 |
. . . . . . . . . . . . 13
⊢ ({𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} ≠ ∅ ↔ ∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵) |
62 | | f1domg 8576 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ Fin → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵)) |
63 | 62 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵)) |
64 | | hashunsng 13846 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))) |
65 | 64 | elv 3404 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
66 | 65 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
67 | 66 | breq1d 5041 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵))) |
68 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin) |
69 | | snfi 8643 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑧} ∈ Fin |
70 | | unfi 8772 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
71 | 68, 69, 70 | sylancl 589 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin) |
72 | | simpl 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐵 ∈ Fin) |
73 | | hashdom 13833 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵)) |
74 | 71, 72, 73 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵)) |
75 | | hashcl 13810 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℕ0) |
76 | 75 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝑦) ∈
ℕ0) |
77 | | nn0p1nn 12016 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑦)
∈ ℕ0 → ((♯‘𝑦) + 1) ∈ ℕ) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝑦) + 1) ∈ ℕ) |
79 | 78 | nnred 11732 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝑦) + 1) ∈ ℝ) |
80 | 55 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝐵) ∈
ℕ0) |
81 | 80 | nn0red 12038 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝐵) ∈ ℝ) |
82 | 79, 81 | lenltd 10865 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (((♯‘𝑦) + 1) ≤ (♯‘𝐵) ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1))) |
83 | 67, 74, 82 | 3bitr3d 312 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝑦 ∪ {𝑧}) ≼ 𝐵 ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1))) |
84 | 63, 83 | sylibd 242 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1))) |
85 | 84 | exlimdv 1939 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1))) |
86 | 61, 85 | syl5bi 245 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ({𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} ≠ ∅ → ¬
(♯‘𝐵) <
((♯‘𝑦) +
1))) |
87 | 86 | necon4ad 2953 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝐵) < ((♯‘𝑦) + 1) → {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} = ∅)) |
88 | 87 | imp 410 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} = ∅) |
89 | 88 | fveq2d 6679 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) =
(♯‘∅)) |
90 | | hashcl 13810 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∪ {𝑧}) ∈ Fin → (♯‘(𝑦 ∪ {𝑧})) ∈
ℕ0) |
91 | 71, 90 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝑦 ∪ {𝑧})) ∈
ℕ0) |
92 | 91 | faccld 13737 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ) |
93 | 92 | nncnd 11733 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ) |
94 | 93 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ) |
95 | 94 | mul01d 10918 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) →
((!‘(♯‘(𝑦
∪ {𝑧}))) · 0) =
0) |
96 | 19, 89, 95 | 3eqtr4a 2799 |
. . . . . . . 8
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0)) |
97 | 66 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
98 | 97 | oveq2d 7187 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1))) |
99 | 80 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) ∈
ℕ0) |
100 | 78 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈
ℕ) |
101 | 100 | nnzd 12168 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈
ℤ) |
102 | | animorr 978 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (((♯‘𝑦) + 1) < 0 ∨
(♯‘𝐵) <
((♯‘𝑦) +
1))) |
103 | | bcval4 13760 |
. . . . . . . . . . 11
⊢
(((♯‘𝐵)
∈ ℕ0 ∧ ((♯‘𝑦) + 1) ∈ ℤ ∧
(((♯‘𝑦) + 1)
< 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1))) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0) |
104 | 99, 101, 102, 103 | syl3anc 1372 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0) |
105 | 98, 104 | eqtrd 2773 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = 0) |
106 | 105 | oveq2d 7187 |
. . . . . . . 8
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) →
((!‘(♯‘(𝑦
∪ {𝑧}))) ·
((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0)) |
107 | 96, 106 | eqtr4d 2776 |
. . . . . . 7
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))) |
108 | 107 | a1d 25 |
. . . . . 6
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))) |
109 | | oveq2 7179 |
. . . . . . 7
⊢
((♯‘{𝑓
∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) → (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))))) |
110 | 68 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝑦 ∈ Fin) |
111 | 72 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝐵 ∈ Fin) |
112 | | simplrr 778 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ¬ 𝑧 ∈ 𝑦) |
113 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) |
114 | 110, 111,
112, 113 | hashf1lem2 13909 |
. . . . . . . 8
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}))) |
115 | 80 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈
ℕ0) |
116 | 115 | faccld 13737 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈
ℕ) |
117 | 116 | nncnd 11733 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈
ℂ) |
118 | 76 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈
ℕ0) |
119 | | peano2nn0 12017 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑦)
∈ ℕ0 → ((♯‘𝑦) + 1) ∈
ℕ0) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈
ℕ0) |
121 | | nn0sub2 12125 |
. . . . . . . . . . . . . . 15
⊢
((((♯‘𝑦)
+ 1) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
((♯‘𝑦) + 1)
≤ (♯‘𝐵))
→ ((♯‘𝐵)
− ((♯‘𝑦)
+ 1)) ∈ ℕ0) |
122 | 120, 115,
113, 121 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈
ℕ0) |
123 | 122 | faccld 13737 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈
ℕ) |
124 | 123 | nncnd 11733 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈
ℂ) |
125 | 123 | nnne0d 11767 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ≠
0) |
126 | 117, 124,
125 | divcld 11495 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) ∈ ℂ) |
127 | 120 | faccld 13737 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈
ℕ) |
128 | 127 | nncnd 11733 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈
ℂ) |
129 | 127 | nnne0d 11767 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ≠ 0) |
130 | 126, 128,
129 | divcan2d 11497 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) /
(!‘((♯‘𝑦)
+ 1)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))))) |
131 | 115 | nn0cnd 12039 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ) |
132 | 118 | nn0cnd 12039 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℂ) |
133 | 131, 132 | subcld 11076 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ) |
134 | | ax-1cn 10674 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
135 | | npcan 10974 |
. . . . . . . . . . . . . 14
⊢
((((♯‘𝐵)
− (♯‘𝑦))
∈ ℂ ∧ 1 ∈ ℂ) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) =
((♯‘𝐵) −
(♯‘𝑦))) |
136 | 133, 134,
135 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) =
((♯‘𝐵) −
(♯‘𝑦))) |
137 | | 1cnd 10715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 1 ∈ ℂ) |
138 | 131, 132,
137 | subsub4d 11107 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) = ((♯‘𝐵) − ((♯‘𝑦) + 1))) |
139 | 138, 122 | eqeltrd 2833 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) ∈
ℕ0) |
140 | | nn0p1nn 12016 |
. . . . . . . . . . . . . 14
⊢
((((♯‘𝐵)
− (♯‘𝑦))
− 1) ∈ ℕ0 → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈
ℕ) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈
ℕ) |
142 | 136, 141 | eqeltrrd 2834 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ) |
143 | 142 | nnne0d 11767 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ≠ 0) |
144 | 126, 133,
143 | divcan2d 11497 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1))))) |
145 | 130, 144 | eqtr4d 2776 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) /
(!‘((♯‘𝑦)
+ 1)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦))))) |
146 | 66 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
147 | 146 | fveq2d 6679 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) = (!‘((♯‘𝑦) + 1))) |
148 | | nn0uz 12363 |
. . . . . . . . . . . . . . 15
⊢
ℕ0 = (ℤ≥‘0) |
149 | 120, 148 | eleqtrdi 2843 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈
(ℤ≥‘0)) |
150 | 115 | nn0zd 12167 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ) |
151 | | elfz5 12991 |
. . . . . . . . . . . . . 14
⊢
((((♯‘𝑦)
+ 1) ∈ (ℤ≥‘0) ∧ (♯‘𝐵) ∈ ℤ) →
(((♯‘𝑦) + 1)
∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵))) |
152 | 149, 150,
151 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝑦) + 1) ∈
(0...(♯‘𝐵))
↔ ((♯‘𝑦) +
1) ≤ (♯‘𝐵))) |
153 | 113, 152 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵))) |
154 | | bcval2 13758 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑦)
+ 1) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ·
(!‘((♯‘𝑦)
+ 1))))) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ·
(!‘((♯‘𝑦)
+ 1))))) |
156 | 146 | oveq2d 7187 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1))) |
157 | 117, 124,
128, 125, 129 | divdiv1d 11526 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / (!‘((♯‘𝑦) + 1))) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ·
(!‘((♯‘𝑦)
+ 1))))) |
158 | 155, 156,
157 | 3eqtr4d 2783 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / (!‘((♯‘𝑦) + 1)))) |
159 | 147, 158 | oveq12d 7189 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘((♯‘𝑦) + 1)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) /
(!‘((♯‘𝑦)
+ 1))))) |
160 | 118, 148 | eleqtrdi 2843 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈
(ℤ≥‘0)) |
161 | | peano2fzr 13012 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝑦)
∈ (ℤ≥‘0) ∧ ((♯‘𝑦) + 1) ∈
(0...(♯‘𝐵)))
→ (♯‘𝑦)
∈ (0...(♯‘𝐵))) |
162 | 160, 153,
161 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (0...(♯‘𝐵))) |
163 | | bcval2 13758 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑦)
∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦))))) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦))))) |
165 | | elfzle2 13003 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑦)
∈ (0...(♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵)) |
166 | 162, 165 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵)) |
167 | | nn0sub2 12125 |
. . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝑦)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
(♯‘𝑦) ≤
(♯‘𝐵)) →
((♯‘𝐵) −
(♯‘𝑦)) ∈
ℕ0) |
168 | 118, 115,
166, 167 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈
ℕ0) |
169 | 168 | faccld 13737 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈
ℕ) |
170 | 169 | nncnd 11733 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈
ℂ) |
171 | 118 | faccld 13737 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈
ℕ) |
172 | 171 | nncnd 11733 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈
ℂ) |
173 | 169 | nnne0d 11767 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ≠ 0) |
174 | 171 | nnne0d 11767 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ≠ 0) |
175 | 117, 170,
172, 173, 174 | divdiv1d 11526 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− (♯‘𝑦)))) / (!‘(♯‘𝑦))) =
((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) ·
(!‘(♯‘𝑦))))) |
176 | 164, 175 | eqtr4d 2776 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− (♯‘𝑦)))) / (!‘(♯‘𝑦)))) |
177 | 176 | oveq2d 7187 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) = ((!‘(♯‘𝑦)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) /
(!‘(♯‘𝑦))))) |
178 | | facnn2 13735 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝐵)
− (♯‘𝑦))
∈ ℕ → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) ·
((♯‘𝐵) −
(♯‘𝑦)))) |
179 | 142, 178 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) =
((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦)))) |
180 | 138 | fveq2d 6679 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) =
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) |
181 | 180 | oveq1d 7186 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) ·
((♯‘𝐵) −
(♯‘𝑦))) =
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))) |
182 | 179, 181 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) =
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))) |
183 | 182 | oveq2d 7187 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− (♯‘𝑦)))) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))) |
184 | 117, 170,
173 | divcld 11495 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− (♯‘𝑦)))) ∈ ℂ) |
185 | 184, 172,
174 | divcan2d 11497 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) /
(!‘(♯‘𝑦)))) = ((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− (♯‘𝑦))))) |
186 | 117, 124,
133, 125, 143 | divdiv1d 11526 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦))) = ((!‘(♯‘𝐵)) /
((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))) |
187 | 183, 185,
186 | 3eqtr4d 2783 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) ·
(((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) /
(!‘(♯‘𝑦)))) = (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) |
188 | 177, 187 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) = (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) |
189 | 188 | oveq2d 7187 |
. . . . . . . . 9
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) /
(!‘((♯‘𝐵)
− ((♯‘𝑦)
+ 1)))) / ((♯‘𝐵) − (♯‘𝑦))))) |
190 | 145, 159,
189 | 3eqtr4d 2783 |
. . . . . . . 8
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))))) |
191 | 114, 190 | eqeq12d 2754 |
. . . . . . 7
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) ↔ (((♯‘𝐵) − (♯‘𝑦)) ·
(♯‘{𝑓 ∣
𝑓:𝑦–1-1→𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦)))))) |
192 | 109, 191 | syl5ibr 249 |
. . . . . 6
⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))) |
193 | 108, 192,
81, 79 | ltlecasei 10827 |
. . . . 5
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))) |
194 | 193 | expcom 417 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝐵 ∈ Fin → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))) |
195 | 194 | a2d 29 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) ·
((♯‘𝐵)C(♯‘𝑦)))) → (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))) |
196 | 27, 36, 45, 54, 60, 195 | findcard2s 8765 |
. 2
⊢ (𝐴 ∈ Fin → (𝐵 ∈ Fin →
(♯‘{𝑓 ∣
𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) ·
((♯‘𝐵)C(♯‘𝐴))))) |
197 | 196 | imp 410 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘{𝑓 ∣
𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) ·
((♯‘𝐵)C(♯‘𝐴)))) |