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

Theorem hashf1 13808
 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 6567 . . . . . . . . 9 (𝑥 = ∅ → (𝑓:𝑥1-1𝐵𝑓:∅–1-1𝐵))
2 f1fn 6572 . . . . . . . . . . . 12 (𝑓:∅–1-1𝐵𝑓 Fn ∅)
3 fn0 6475 . . . . . . . . . . . 12 (𝑓 Fn ∅ ↔ 𝑓 = ∅)
42, 3sylib 219 . . . . . . . . . . 11 (𝑓:∅–1-1𝐵𝑓 = ∅)
5 f10 6643 . . . . . . . . . . . 12 ∅:∅–1-1𝐵
6 f1eq1 6566 . . . . . . . . . . . 12 (𝑓 = ∅ → (𝑓:∅–1-1𝐵 ↔ ∅:∅–1-1𝐵))
75, 6mpbiri 259 . . . . . . . . . . 11 (𝑓 = ∅ → 𝑓:∅–1-1𝐵)
84, 7impbii 210 . . . . . . . . . 10 (𝑓:∅–1-1𝐵𝑓 = ∅)
9 velsn 4579 . . . . . . . . . 10 (𝑓 ∈ {∅} ↔ 𝑓 = ∅)
108, 9bitr4i 279 . . . . . . . . 9 (𝑓:∅–1-1𝐵𝑓 ∈ {∅})
111, 10syl6bb 288 . . . . . . . 8 (𝑥 = ∅ → (𝑓:𝑥1-1𝐵𝑓 ∈ {∅}))
1211abbi1dv 2956 . . . . . . 7 (𝑥 = ∅ → {𝑓𝑓:𝑥1-1𝐵} = {∅})
1312fveq2d 6670 . . . . . 6 (𝑥 = ∅ → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{∅}))
14 0ex 5207 . . . . . . 7 ∅ ∈ V
15 hashsng 13723 . . . . . . 7 (∅ ∈ V → (♯‘{∅}) = 1)
1614, 15ax-mp 5 . . . . . 6 (♯‘{∅}) = 1
1713, 16syl6eq 2876 . . . . 5 (𝑥 = ∅ → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = 1)
18 fveq2 6666 . . . . . . . . 9 (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
19 hash0 13721 . . . . . . . . 9 (♯‘∅) = 0
2018, 19syl6eq 2876 . . . . . . . 8 (𝑥 = ∅ → (♯‘𝑥) = 0)
2120fveq2d 6670 . . . . . . 7 (𝑥 = ∅ → (!‘(♯‘𝑥)) = (!‘0))
22 fac0 13629 . . . . . . 7 (!‘0) = 1
2321, 22syl6eq 2876 . . . . . 6 (𝑥 = ∅ → (!‘(♯‘𝑥)) = 1)
2420oveq2d 7167 . . . . . 6 (𝑥 = ∅ → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C0))
2523, 24oveq12d 7169 . . . . 5 (𝑥 = ∅ → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = (1 · ((♯‘𝐵)C0)))
2617, 25eqeq12d 2841 . . . 4 (𝑥 = ∅ → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ 1 = (1 · ((♯‘𝐵)C0))))
2726imbi2d 342 . . 3 (𝑥 = ∅ → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → 1 = (1 · ((♯‘𝐵)C0)))))
28 f1eq2 6567 . . . . . . 7 (𝑥 = 𝑦 → (𝑓:𝑥1-1𝐵𝑓:𝑦1-1𝐵))
2928abbidv 2889 . . . . . 6 (𝑥 = 𝑦 → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:𝑦1-1𝐵})
3029fveq2d 6670 . . . . 5 (𝑥 = 𝑦 → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:𝑦1-1𝐵}))
31 2fveq3 6671 . . . . . 6 (𝑥 = 𝑦 → (!‘(♯‘𝑥)) = (!‘(♯‘𝑦)))
32 fveq2 6666 . . . . . . 7 (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
3332oveq2d 7167 . . . . . 6 (𝑥 = 𝑦 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝑦)))
3431, 33oveq12d 7169 . . . . 5 (𝑥 = 𝑦 → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))
3530, 34eqeq12d 2841 . . . 4 (𝑥 = 𝑦 → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
3635imbi2d 342 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))))
37 f1eq2 6567 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓:𝑥1-1𝐵𝑓:(𝑦 ∪ {𝑧})–1-1𝐵))
3837abbidv 2889 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵})
3938fveq2d 6670 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}))
40 2fveq3 6671 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (!‘(♯‘𝑥)) = (!‘(♯‘(𝑦 ∪ {𝑧}))))
41 fveq2 6666 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
4241oveq2d 7167 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))
4340, 42oveq12d 7169 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))
4439, 43eqeq12d 2841 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
4544imbi2d 342 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))))
46 f1eq2 6567 . . . . . . 7 (𝑥 = 𝐴 → (𝑓:𝑥1-1𝐵𝑓:𝐴1-1𝐵))
4746abbidv 2889 . . . . . 6 (𝑥 = 𝐴 → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:𝐴1-1𝐵})
4847fveq2d 6670 . . . . 5 (𝑥 = 𝐴 → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:𝐴1-1𝐵}))
49 2fveq3 6671 . . . . . 6 (𝑥 = 𝐴 → (!‘(♯‘𝑥)) = (!‘(♯‘𝐴)))
50 fveq2 6666 . . . . . . 7 (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴))
5150oveq2d 7167 . . . . . 6 (𝑥 = 𝐴 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝐴)))
5249, 51oveq12d 7169 . . . . 5 (𝑥 = 𝐴 → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))
5348, 52eqeq12d 2841 . . . 4 (𝑥 = 𝐴 → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴)))))
5453imbi2d 342 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))))
55 hashcl 13710 . . . . . 6 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
56 bcn0 13663 . . . . . 6 ((♯‘𝐵) ∈ ℕ0 → ((♯‘𝐵)C0) = 1)
5755, 56syl 17 . . . . 5 (𝐵 ∈ Fin → ((♯‘𝐵)C0) = 1)
5857oveq2d 7167 . . . 4 (𝐵 ∈ Fin → (1 · ((♯‘𝐵)C0)) = (1 · 1))
59 1t1e1 11791 . . . 4 (1 · 1) = 1
6058, 59syl6req 2877 . . 3 (𝐵 ∈ Fin → 1 = (1 · ((♯‘𝐵)C0)))
61 abn0 4339 . . . . . . . . . . . . 13 ({𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} ≠ ∅ ↔ ∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1𝐵)
62 f1domg 8521 . . . . . . . . . . . . . . . 16 (𝐵 ∈ Fin → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
6362adantr 481 . . . . . . . . . . . . . . 15 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
64 hashunsng 13746 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
6564elv 3504 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
6665adantl 482 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
6766breq1d 5072 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
68 simprl 767 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ∈ Fin)
69 snfi 8586 . . . . . . . . . . . . . . . . . 18 {𝑧} ∈ Fin
70 unfi 8777 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
7168, 69, 70sylancl 586 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin)
72 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝐵 ∈ Fin)
73 hashdom 13733 . . . . . . . . . . . . . . . . 17 (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
7471, 72, 73syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
75 hashcl 13710 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ0)
7675ad2antrl 724 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝑦) ∈ ℕ0)
77 nn0p1nn 11928 . . . . . . . . . . . . . . . . . . 19 ((♯‘𝑦) ∈ ℕ0 → ((♯‘𝑦) + 1) ∈ ℕ)
7876, 77syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝑦) + 1) ∈ ℕ)
7978nnred 11645 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝑦) + 1) ∈ ℝ)
8055adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝐵) ∈ ℕ0)
8180nn0red 11948 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝐵) ∈ ℝ)
8279, 81lenltd 10778 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (((♯‘𝑦) + 1) ≤ (♯‘𝐵) ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8367, 74, 823bitr3d 310 . . . . . . . . . . . . . . 15 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝑦 ∪ {𝑧}) ≼ 𝐵 ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8463, 83sylibd 240 . . . . . . . . . . . . . 14 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8584exlimdv 1927 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8661, 85syl5bi 243 . . . . . . . . . . . 12 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ({𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} ≠ ∅ → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8786necon4ad 3039 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝐵) < ((♯‘𝑦) + 1) → {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} = ∅))
8887imp 407 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} = ∅)
8988fveq2d 6670 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = (♯‘∅))
90 hashcl 13710 . . . . . . . . . . . . . 14 ((𝑦 ∪ {𝑧}) ∈ Fin → (♯‘(𝑦 ∪ {𝑧})) ∈ ℕ0)
9171, 90syl 17 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝑦 ∪ {𝑧})) ∈ ℕ0)
9291faccld 13637 . . . . . . . . . . . 12 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
9392nncnd 11646 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
9493adantr 481 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
9594mul01d 10831 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0) = 0)
9619, 89, 953eqtr4a 2886 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0))
9766adantr 481 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
9897oveq2d 7167 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1)))
9980adantr 481 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) ∈ ℕ0)
10078adantr 481 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈ ℕ)
101100nnzd 12078 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈ ℤ)
102 animorr 974 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (((♯‘𝑦) + 1) < 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1)))
103 bcval4 13660 . . . . . . . . . . 11 (((♯‘𝐵) ∈ ℕ0 ∧ ((♯‘𝑦) + 1) ∈ ℤ ∧ (((♯‘𝑦) + 1) < 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1))) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0)
10499, 101, 102, 103syl3anc 1365 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0)
10598, 104eqtrd 2860 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = 0)
106105oveq2d 7167 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0))
10796, 106eqtr4d 2863 . . . . . . 7 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))
108107a1d 25 . . . . . 6 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
109 oveq2 7159 . . . . . . 7 ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
11068adantr 481 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝑦 ∈ Fin)
11172adantr 481 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝐵 ∈ Fin)
112 simplrr 774 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ¬ 𝑧𝑦)
113 simpr 485 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ≤ (♯‘𝐵))
114110, 111, 112, 113hashf1lem2 13807 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})))
11580adantr 481 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
116115faccld 13637 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈ ℕ)
117116nncnd 11646 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈ ℂ)
11876adantr 481 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℕ0)
119 peano2nn0 11929 . . . . . . . . . . . . . . . 16 ((♯‘𝑦) ∈ ℕ0 → ((♯‘𝑦) + 1) ∈ ℕ0)
120118, 119syl 17 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ ℕ0)
121 nn0sub2 12035 . . . . . . . . . . . . . . 15 ((((♯‘𝑦) + 1) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ0)
122120, 115, 113, 121syl3anc 1365 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ0)
123122faccld 13637 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℕ)
124123nncnd 11646 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℂ)
125123nnne0d 11679 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ≠ 0)
126117, 124, 125divcld 11408 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) ∈ ℂ)
127120faccld 13637 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈ ℕ)
128127nncnd 11646 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈ ℂ)
129127nnne0d 11679 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ≠ 0)
130126, 128, 129divcan2d 11410 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))))
131115nn0cnd 11949 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ)
132118nn0cnd 11949 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℂ)
133131, 132subcld 10989 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ)
134 ax-1cn 10587 . . . . . . . . . . . . . 14 1 ∈ ℂ
135 npcan 10887 . . . . . . . . . . . . . 14 ((((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) = ((♯‘𝐵) − (♯‘𝑦)))
136133, 134, 135sylancl 586 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) = ((♯‘𝐵) − (♯‘𝑦)))
137 1cnd 10628 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 1 ∈ ℂ)
138131, 132, 137subsub4d 11020 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) = ((♯‘𝐵) − ((♯‘𝑦) + 1)))
139138, 122eqeltrd 2917 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) ∈ ℕ0)
140 nn0p1nn 11928 . . . . . . . . . . . . . 14 ((((♯‘𝐵) − (♯‘𝑦)) − 1) ∈ ℕ0 → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈ ℕ)
141139, 140syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈ ℕ)
142136, 141eqeltrrd 2918 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ)
143142nnne0d 11679 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ≠ 0)
144126, 133, 143divcan2d 11410 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))))
145130, 144eqtr4d 2863 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))))
14666adantr 481 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
147146fveq2d 6670 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) = (!‘((♯‘𝑦) + 1)))
148 nn0uz 12272 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
149120, 148syl6eleq 2927 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (ℤ‘0))
150115nn0zd 12077 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
151 elfz5 12893 . . . . . . . . . . . . . 14 ((((♯‘𝑦) + 1) ∈ (ℤ‘0) ∧ (♯‘𝐵) ∈ ℤ) → (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
152149, 150, 151syl2anc 584 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
153113, 152mpbird 258 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)))
154 bcval2 13658 . . . . . . . . . . . 12 (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
155153, 154syl 17 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
156146oveq2d 7167 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1)))
157117, 124, 128, 125, 129divdiv1d 11439 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
158155, 156, 1573eqtr4d 2870 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1))))
159147, 158oveq12d 7169 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))))
160118, 148syl6eleq 2927 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (ℤ‘0))
161 peano2fzr 12913 . . . . . . . . . . . . . . 15 (((♯‘𝑦) ∈ (ℤ‘0) ∧ ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵))) → (♯‘𝑦) ∈ (0...(♯‘𝐵)))
162160, 153, 161syl2anc 584 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (0...(♯‘𝐵)))
163 bcval2 13658 . . . . . . . . . . . . . 14 ((♯‘𝑦) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
164162, 163syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
165 elfzle2 12904 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑦) ∈ (0...(♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵))
166162, 165syl 17 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵))
167 nn0sub2 12035 . . . . . . . . . . . . . . . . 17 (((♯‘𝑦) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝑦) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ0)
168118, 115, 166, 167syl3anc 1365 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ0)
169168faccld 13637 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℕ)
170169nncnd 11646 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℂ)
171118faccld 13637 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈ ℕ)
172171nncnd 11646 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈ ℂ)
173169nnne0d 11679 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ≠ 0)
174171nnne0d 11679 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ≠ 0)
175117, 170, 172, 173, 174divdiv1d 11439 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
176164, 175eqtr4d 2863 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦))))
177176oveq2d 7167 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) = ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))))
178 facnn2 13635 . . . . . . . . . . . . . . 15 (((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))))
179142, 178syl 17 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))))
180138fveq2d 6670 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) = (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))))
181180oveq1d 7166 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))) = ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))
182179, 181eqtrd 2860 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))
183182oveq2d 7167 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))))
184117, 170, 173divcld 11408 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) ∈ ℂ)
185184, 172, 174divcan2d 11410 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))))
186117, 124, 133, 125, 143divdiv1d 11439 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))))
187183, 185, 1863eqtr4d 2870 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))))
188177, 187eqtrd 2860 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))))
189188oveq2d 7167 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))))
190145, 159, 1893eqtr4d 2870 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
191114, 190eqeq12d 2841 . . . . . . 7 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) ↔ (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))))
192109, 191syl5ibr 247 . . . . . 6 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
193108, 192, 81, 79ltlecasei 10740 . . . . 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 8751 . 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 207   ∧ wa 396   ∨ wo 843   = wceq 1530  ∃wex 1773   ∈ wcel 2107  {cab 2803   ≠ wne 3020  Vcvv 3499   ∪ cun 3937  ∅c0 4294  {csn 4563   class class class wbr 5062   Fn wfn 6346  –1-1→wf1 6348  ‘cfv 6351  (class class class)co 7151   ≼ cdom 8499  Fincfn 8501  ℂcc 10527  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   < clt 10667   ≤ cle 10668   − cmin 10862   / cdiv 11289  ℕcn 11630  ℕ0cn0 11889  ℤcz 11973  ℤ≥cuz 12235  ...cfz 12885  !cfa 13626  Ccbc 13655  ♯chash 13683 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8282  df-map 8401  df-pm 8402  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-dju 9322  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-n0 11890  df-xnn0 11960  df-z 11974  df-uz 12236  df-fz 12886  df-seq 13363  df-fac 13627  df-bc 13656  df-hash 13684 This theorem is referenced by:  hashfac  13809  birthdaylem2  25446
 Copyright terms: Public domain W3C validator