MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashf1 Structured version   Visualization version   GIF version

Theorem hashf1 14171
Description: The permutation number 𝐴 ∣ ! · ( ∣ 𝐵 ∣ C ∣ 𝐴 ∣ ) = 𝐵 ∣ ! / ( ∣ 𝐵 ∣ − ∣ 𝐴 ∣ )! counts the number of injections from 𝐴 to 𝐵. (Contributed by Mario Carneiro, 21-Jan-2015.)
Assertion
Ref Expression
hashf1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓

Proof of Theorem hashf1
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1eq2 6666 . . . . . . . . 9 (𝑥 = ∅ → (𝑓:𝑥1-1𝐵𝑓:∅–1-1𝐵))
2 f1fn 6671 . . . . . . . . . . . 12 (𝑓:∅–1-1𝐵𝑓 Fn ∅)
3 fn0 6564 . . . . . . . . . . . 12 (𝑓 Fn ∅ ↔ 𝑓 = ∅)
42, 3sylib 217 . . . . . . . . . . 11 (𝑓:∅–1-1𝐵𝑓 = ∅)
5 f10 6749 . . . . . . . . . . . 12 ∅:∅–1-1𝐵
6 f1eq1 6665 . . . . . . . . . . . 12 (𝑓 = ∅ → (𝑓:∅–1-1𝐵 ↔ ∅:∅–1-1𝐵))
75, 6mpbiri 257 . . . . . . . . . . 11 (𝑓 = ∅ → 𝑓:∅–1-1𝐵)
84, 7impbii 208 . . . . . . . . . 10 (𝑓:∅–1-1𝐵𝑓 = ∅)
9 velsn 4577 . . . . . . . . . 10 (𝑓 ∈ {∅} ↔ 𝑓 = ∅)
108, 9bitr4i 277 . . . . . . . . 9 (𝑓:∅–1-1𝐵𝑓 ∈ {∅})
111, 10bitrdi 287 . . . . . . . 8 (𝑥 = ∅ → (𝑓:𝑥1-1𝐵𝑓 ∈ {∅}))
1211abbi1dv 2878 . . . . . . 7 (𝑥 = ∅ → {𝑓𝑓:𝑥1-1𝐵} = {∅})
1312fveq2d 6778 . . . . . 6 (𝑥 = ∅ → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{∅}))
14 0ex 5231 . . . . . . 7 ∅ ∈ V
15 hashsng 14084 . . . . . . 7 (∅ ∈ V → (♯‘{∅}) = 1)
1614, 15ax-mp 5 . . . . . 6 (♯‘{∅}) = 1
1713, 16eqtrdi 2794 . . . . 5 (𝑥 = ∅ → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = 1)
18 fveq2 6774 . . . . . . . . 9 (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
19 hash0 14082 . . . . . . . . 9 (♯‘∅) = 0
2018, 19eqtrdi 2794 . . . . . . . 8 (𝑥 = ∅ → (♯‘𝑥) = 0)
2120fveq2d 6778 . . . . . . 7 (𝑥 = ∅ → (!‘(♯‘𝑥)) = (!‘0))
22 fac0 13990 . . . . . . 7 (!‘0) = 1
2321, 22eqtrdi 2794 . . . . . 6 (𝑥 = ∅ → (!‘(♯‘𝑥)) = 1)
2420oveq2d 7291 . . . . . 6 (𝑥 = ∅ → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C0))
2523, 24oveq12d 7293 . . . . 5 (𝑥 = ∅ → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = (1 · ((♯‘𝐵)C0)))
2617, 25eqeq12d 2754 . . . 4 (𝑥 = ∅ → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ 1 = (1 · ((♯‘𝐵)C0))))
2726imbi2d 341 . . 3 (𝑥 = ∅ → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → 1 = (1 · ((♯‘𝐵)C0)))))
28 f1eq2 6666 . . . . . . 7 (𝑥 = 𝑦 → (𝑓:𝑥1-1𝐵𝑓:𝑦1-1𝐵))
2928abbidv 2807 . . . . . 6 (𝑥 = 𝑦 → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:𝑦1-1𝐵})
3029fveq2d 6778 . . . . 5 (𝑥 = 𝑦 → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:𝑦1-1𝐵}))
31 2fveq3 6779 . . . . . 6 (𝑥 = 𝑦 → (!‘(♯‘𝑥)) = (!‘(♯‘𝑦)))
32 fveq2 6774 . . . . . . 7 (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
3332oveq2d 7291 . . . . . 6 (𝑥 = 𝑦 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝑦)))
3431, 33oveq12d 7293 . . . . 5 (𝑥 = 𝑦 → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))
3530, 34eqeq12d 2754 . . . 4 (𝑥 = 𝑦 → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
3635imbi2d 341 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))))
37 f1eq2 6666 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓:𝑥1-1𝐵𝑓:(𝑦 ∪ {𝑧})–1-1𝐵))
3837abbidv 2807 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵})
3938fveq2d 6778 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}))
40 2fveq3 6779 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (!‘(♯‘𝑥)) = (!‘(♯‘(𝑦 ∪ {𝑧}))))
41 fveq2 6774 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
4241oveq2d 7291 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))
4340, 42oveq12d 7293 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))
4439, 43eqeq12d 2754 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
4544imbi2d 341 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))))
46 f1eq2 6666 . . . . . . 7 (𝑥 = 𝐴 → (𝑓:𝑥1-1𝐵𝑓:𝐴1-1𝐵))
4746abbidv 2807 . . . . . 6 (𝑥 = 𝐴 → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:𝐴1-1𝐵})
4847fveq2d 6778 . . . . 5 (𝑥 = 𝐴 → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:𝐴1-1𝐵}))
49 2fveq3 6779 . . . . . 6 (𝑥 = 𝐴 → (!‘(♯‘𝑥)) = (!‘(♯‘𝐴)))
50 fveq2 6774 . . . . . . 7 (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴))
5150oveq2d 7291 . . . . . 6 (𝑥 = 𝐴 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝐴)))
5249, 51oveq12d 7293 . . . . 5 (𝑥 = 𝐴 → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))
5348, 52eqeq12d 2754 . . . 4 (𝑥 = 𝐴 → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴)))))
5453imbi2d 341 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))))
55 hashcl 14071 . . . . . 6 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
56 bcn0 14024 . . . . . 6 ((♯‘𝐵) ∈ ℕ0 → ((♯‘𝐵)C0) = 1)
5755, 56syl 17 . . . . 5 (𝐵 ∈ Fin → ((♯‘𝐵)C0) = 1)
5857oveq2d 7291 . . . 4 (𝐵 ∈ Fin → (1 · ((♯‘𝐵)C0)) = (1 · 1))
59 1t1e1 12135 . . . 4 (1 · 1) = 1
6058, 59eqtr2di 2795 . . 3 (𝐵 ∈ Fin → 1 = (1 · ((♯‘𝐵)C0)))
61 abn0 4314 . . . . . . . . . . . . 13 ({𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} ≠ ∅ ↔ ∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1𝐵)
62 f1domg 8760 . . . . . . . . . . . . . . . 16 (𝐵 ∈ Fin → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
6362adantr 481 . . . . . . . . . . . . . . 15 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
64 hashunsng 14107 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
6564elv 3438 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
6665adantl 482 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
6766breq1d 5084 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
68 simprl 768 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ∈ Fin)
69 snfi 8834 . . . . . . . . . . . . . . . . . 18 {𝑧} ∈ Fin
70 unfi 8955 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
7168, 69, 70sylancl 586 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin)
72 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝐵 ∈ Fin)
73 hashdom 14094 . . . . . . . . . . . . . . . . 17 (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
7471, 72, 73syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
75 hashcl 14071 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ0)
7675ad2antrl 725 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝑦) ∈ ℕ0)
77 nn0p1nn 12272 . . . . . . . . . . . . . . . . . . 19 ((♯‘𝑦) ∈ ℕ0 → ((♯‘𝑦) + 1) ∈ ℕ)
7876, 77syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝑦) + 1) ∈ ℕ)
7978nnred 11988 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝑦) + 1) ∈ ℝ)
8055adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝐵) ∈ ℕ0)
8180nn0red 12294 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝐵) ∈ ℝ)
8279, 81lenltd 11121 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (((♯‘𝑦) + 1) ≤ (♯‘𝐵) ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8367, 74, 823bitr3d 309 . . . . . . . . . . . . . . 15 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝑦 ∪ {𝑧}) ≼ 𝐵 ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8463, 83sylibd 238 . . . . . . . . . . . . . 14 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8584exlimdv 1936 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8661, 85syl5bi 241 . . . . . . . . . . . 12 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ({𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} ≠ ∅ → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8786necon4ad 2962 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝐵) < ((♯‘𝑦) + 1) → {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} = ∅))
8887imp 407 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} = ∅)
8988fveq2d 6778 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = (♯‘∅))
90 hashcl 14071 . . . . . . . . . . . . . 14 ((𝑦 ∪ {𝑧}) ∈ Fin → (♯‘(𝑦 ∪ {𝑧})) ∈ ℕ0)
9171, 90syl 17 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝑦 ∪ {𝑧})) ∈ ℕ0)
9291faccld 13998 . . . . . . . . . . . 12 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
9392nncnd 11989 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
9493adantr 481 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
9594mul01d 11174 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0) = 0)
9619, 89, 953eqtr4a 2804 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0))
9766adantr 481 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
9897oveq2d 7291 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1)))
9980adantr 481 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) ∈ ℕ0)
10078adantr 481 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈ ℕ)
101100nnzd 12425 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈ ℤ)
102 animorr 976 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (((♯‘𝑦) + 1) < 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1)))
103 bcval4 14021 . . . . . . . . . . 11 (((♯‘𝐵) ∈ ℕ0 ∧ ((♯‘𝑦) + 1) ∈ ℤ ∧ (((♯‘𝑦) + 1) < 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1))) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0)
10499, 101, 102, 103syl3anc 1370 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0)
10598, 104eqtrd 2778 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = 0)
106105oveq2d 7291 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0))
10796, 106eqtr4d 2781 . . . . . . 7 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))
108107a1d 25 . . . . . 6 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
109 oveq2 7283 . . . . . . 7 ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
11068adantr 481 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝑦 ∈ Fin)
11172adantr 481 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝐵 ∈ Fin)
112 simplrr 775 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ¬ 𝑧𝑦)
113 simpr 485 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ≤ (♯‘𝐵))
114110, 111, 112, 113hashf1lem2 14170 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})))
11580adantr 481 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
116115faccld 13998 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈ ℕ)
117116nncnd 11989 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈ ℂ)
11876adantr 481 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℕ0)
119 peano2nn0 12273 . . . . . . . . . . . . . . . 16 ((♯‘𝑦) ∈ ℕ0 → ((♯‘𝑦) + 1) ∈ ℕ0)
120118, 119syl 17 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ ℕ0)
121 nn0sub2 12381 . . . . . . . . . . . . . . 15 ((((♯‘𝑦) + 1) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ0)
122120, 115, 113, 121syl3anc 1370 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ0)
123122faccld 13998 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℕ)
124123nncnd 11989 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℂ)
125123nnne0d 12023 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ≠ 0)
126117, 124, 125divcld 11751 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) ∈ ℂ)
127120faccld 13998 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈ ℕ)
128127nncnd 11989 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈ ℂ)
129127nnne0d 12023 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ≠ 0)
130126, 128, 129divcan2d 11753 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))))
131115nn0cnd 12295 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ)
132118nn0cnd 12295 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℂ)
133131, 132subcld 11332 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ)
134 ax-1cn 10929 . . . . . . . . . . . . . 14 1 ∈ ℂ
135 npcan 11230 . . . . . . . . . . . . . 14 ((((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) = ((♯‘𝐵) − (♯‘𝑦)))
136133, 134, 135sylancl 586 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) = ((♯‘𝐵) − (♯‘𝑦)))
137 1cnd 10970 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 1 ∈ ℂ)
138131, 132, 137subsub4d 11363 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) = ((♯‘𝐵) − ((♯‘𝑦) + 1)))
139138, 122eqeltrd 2839 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) ∈ ℕ0)
140 nn0p1nn 12272 . . . . . . . . . . . . . 14 ((((♯‘𝐵) − (♯‘𝑦)) − 1) ∈ ℕ0 → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈ ℕ)
141139, 140syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈ ℕ)
142136, 141eqeltrrd 2840 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ)
143142nnne0d 12023 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ≠ 0)
144126, 133, 143divcan2d 11753 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))))
145130, 144eqtr4d 2781 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))))
14666adantr 481 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
147146fveq2d 6778 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) = (!‘((♯‘𝑦) + 1)))
148 nn0uz 12620 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
149120, 148eleqtrdi 2849 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (ℤ‘0))
150115nn0zd 12424 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
151 elfz5 13248 . . . . . . . . . . . . . 14 ((((♯‘𝑦) + 1) ∈ (ℤ‘0) ∧ (♯‘𝐵) ∈ ℤ) → (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
152149, 150, 151syl2anc 584 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
153113, 152mpbird 256 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)))
154 bcval2 14019 . . . . . . . . . . . 12 (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
155153, 154syl 17 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
156146oveq2d 7291 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1)))
157117, 124, 128, 125, 129divdiv1d 11782 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
158155, 156, 1573eqtr4d 2788 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1))))
159147, 158oveq12d 7293 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))))
160118, 148eleqtrdi 2849 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (ℤ‘0))
161 peano2fzr 13269 . . . . . . . . . . . . . . 15 (((♯‘𝑦) ∈ (ℤ‘0) ∧ ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵))) → (♯‘𝑦) ∈ (0...(♯‘𝐵)))
162160, 153, 161syl2anc 584 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (0...(♯‘𝐵)))
163 bcval2 14019 . . . . . . . . . . . . . 14 ((♯‘𝑦) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
164162, 163syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
165 elfzle2 13260 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑦) ∈ (0...(♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵))
166162, 165syl 17 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵))
167 nn0sub2 12381 . . . . . . . . . . . . . . . . 17 (((♯‘𝑦) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝑦) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ0)
168118, 115, 166, 167syl3anc 1370 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ0)
169168faccld 13998 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℕ)
170169nncnd 11989 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℂ)
171118faccld 13998 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈ ℕ)
172171nncnd 11989 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈ ℂ)
173169nnne0d 12023 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ≠ 0)
174171nnne0d 12023 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ≠ 0)
175117, 170, 172, 173, 174divdiv1d 11782 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
176164, 175eqtr4d 2781 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦))))
177176oveq2d 7291 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) = ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))))
178 facnn2 13996 . . . . . . . . . . . . . . 15 (((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))))
179142, 178syl 17 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))))
180138fveq2d 6778 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) = (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))))
181180oveq1d 7290 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))) = ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))
182179, 181eqtrd 2778 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))
183182oveq2d 7291 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))))
184117, 170, 173divcld 11751 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) ∈ ℂ)
185184, 172, 174divcan2d 11753 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))))
186117, 124, 133, 125, 143divdiv1d 11782 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))))
187183, 185, 1863eqtr4d 2788 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))))
188177, 187eqtrd 2778 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))))
189188oveq2d 7291 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))))
190145, 159, 1893eqtr4d 2788 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
191114, 190eqeq12d 2754 . . . . . . 7 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) ↔ (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))))
192109, 191syl5ibr 245 . . . . . 6 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
193108, 192, 81, 79ltlecasei 11083 . . . . 5 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
194193expcom 414 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝐵 ∈ Fin → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))))
195194a2d 29 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))) → (𝐵 ∈ Fin → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))))
19627, 36, 45, 54, 60, 195findcard2s 8948 . 2 (𝐴 ∈ Fin → (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴)))))
197196imp 407 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844   = wceq 1539  wex 1782  wcel 2106  {cab 2715  wne 2943  Vcvv 3432  cun 3885  c0 4256  {csn 4561   class class class wbr 5074   Fn wfn 6428  1-1wf1 6430  cfv 6433  (class class class)co 7275  cdom 8731  Fincfn 8733  cc 10869  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876   < clt 11009  cle 11010  cmin 11205   / cdiv 11632  cn 11973  0cn0 12233  cz 12319  cuz 12582  ...cfz 13239  !cfa 13987  Ccbc 14016  chash 14044
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-oadd 8301  df-er 8498  df-map 8617  df-pm 8618  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-dju 9659  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-n0 12234  df-xnn0 12306  df-z 12320  df-uz 12583  df-fz 13240  df-seq 13722  df-fac 13988  df-bc 14017  df-hash 14045
This theorem is referenced by:  hashfac  14172  birthdaylem2  26102
  Copyright terms: Public domain W3C validator