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

Theorem hashf1 13445
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 6281 . . . . . . . . 9 (𝑥 = ∅ → (𝑓:𝑥1-1𝐵𝑓:∅–1-1𝐵))
2 f1fn 6286 . . . . . . . . . . . 12 (𝑓:∅–1-1𝐵𝑓 Fn ∅)
3 fn0 6191 . . . . . . . . . . . 12 (𝑓 Fn ∅ ↔ 𝑓 = ∅)
42, 3sylib 209 . . . . . . . . . . 11 (𝑓:∅–1-1𝐵𝑓 = ∅)
5 f10 6354 . . . . . . . . . . . 12 ∅:∅–1-1𝐵
6 f1eq1 6280 . . . . . . . . . . . 12 (𝑓 = ∅ → (𝑓:∅–1-1𝐵 ↔ ∅:∅–1-1𝐵))
75, 6mpbiri 249 . . . . . . . . . . 11 (𝑓 = ∅ → 𝑓:∅–1-1𝐵)
84, 7impbii 200 . . . . . . . . . 10 (𝑓:∅–1-1𝐵𝑓 = ∅)
9 velsn 4352 . . . . . . . . . 10 (𝑓 ∈ {∅} ↔ 𝑓 = ∅)
108, 9bitr4i 269 . . . . . . . . 9 (𝑓:∅–1-1𝐵𝑓 ∈ {∅})
111, 10syl6bb 278 . . . . . . . 8 (𝑥 = ∅ → (𝑓:𝑥1-1𝐵𝑓 ∈ {∅}))
1211abbi1dv 2886 . . . . . . 7 (𝑥 = ∅ → {𝑓𝑓:𝑥1-1𝐵} = {∅})
1312fveq2d 6381 . . . . . 6 (𝑥 = ∅ → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{∅}))
14 0ex 4952 . . . . . . 7 ∅ ∈ V
15 hashsng 13364 . . . . . . 7 (∅ ∈ V → (♯‘{∅}) = 1)
1614, 15ax-mp 5 . . . . . 6 (♯‘{∅}) = 1
1713, 16syl6eq 2815 . . . . 5 (𝑥 = ∅ → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = 1)
18 fveq2 6377 . . . . . . . . 9 (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
19 hash0 13363 . . . . . . . . 9 (♯‘∅) = 0
2018, 19syl6eq 2815 . . . . . . . 8 (𝑥 = ∅ → (♯‘𝑥) = 0)
2120fveq2d 6381 . . . . . . 7 (𝑥 = ∅ → (!‘(♯‘𝑥)) = (!‘0))
22 fac0 13270 . . . . . . 7 (!‘0) = 1
2321, 22syl6eq 2815 . . . . . 6 (𝑥 = ∅ → (!‘(♯‘𝑥)) = 1)
2420oveq2d 6860 . . . . . 6 (𝑥 = ∅ → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C0))
2523, 24oveq12d 6862 . . . . 5 (𝑥 = ∅ → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = (1 · ((♯‘𝐵)C0)))
2617, 25eqeq12d 2780 . . . 4 (𝑥 = ∅ → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ 1 = (1 · ((♯‘𝐵)C0))))
2726imbi2d 331 . . 3 (𝑥 = ∅ → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → 1 = (1 · ((♯‘𝐵)C0)))))
28 f1eq2 6281 . . . . . . 7 (𝑥 = 𝑦 → (𝑓:𝑥1-1𝐵𝑓:𝑦1-1𝐵))
2928abbidv 2884 . . . . . 6 (𝑥 = 𝑦 → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:𝑦1-1𝐵})
3029fveq2d 6381 . . . . 5 (𝑥 = 𝑦 → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:𝑦1-1𝐵}))
31 2fveq3 6382 . . . . . 6 (𝑥 = 𝑦 → (!‘(♯‘𝑥)) = (!‘(♯‘𝑦)))
32 fveq2 6377 . . . . . . 7 (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
3332oveq2d 6860 . . . . . 6 (𝑥 = 𝑦 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝑦)))
3431, 33oveq12d 6862 . . . . 5 (𝑥 = 𝑦 → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))
3530, 34eqeq12d 2780 . . . 4 (𝑥 = 𝑦 → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
3635imbi2d 331 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))))
37 f1eq2 6281 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓:𝑥1-1𝐵𝑓:(𝑦 ∪ {𝑧})–1-1𝐵))
3837abbidv 2884 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵})
3938fveq2d 6381 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}))
40 2fveq3 6382 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (!‘(♯‘𝑥)) = (!‘(♯‘(𝑦 ∪ {𝑧}))))
41 fveq2 6377 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
4241oveq2d 6860 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))
4340, 42oveq12d 6862 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))
4439, 43eqeq12d 2780 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
4544imbi2d 331 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))))
46 f1eq2 6281 . . . . . . 7 (𝑥 = 𝐴 → (𝑓:𝑥1-1𝐵𝑓:𝐴1-1𝐵))
4746abbidv 2884 . . . . . 6 (𝑥 = 𝐴 → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:𝐴1-1𝐵})
4847fveq2d 6381 . . . . 5 (𝑥 = 𝐴 → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:𝐴1-1𝐵}))
49 2fveq3 6382 . . . . . 6 (𝑥 = 𝐴 → (!‘(♯‘𝑥)) = (!‘(♯‘𝐴)))
50 fveq2 6377 . . . . . . 7 (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴))
5150oveq2d 6860 . . . . . 6 (𝑥 = 𝐴 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝐴)))
5249, 51oveq12d 6862 . . . . 5 (𝑥 = 𝐴 → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))
5348, 52eqeq12d 2780 . . . 4 (𝑥 = 𝐴 → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴)))))
5453imbi2d 331 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))))
55 hashcl 13352 . . . . . 6 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
56 bcn0 13304 . . . . . 6 ((♯‘𝐵) ∈ ℕ0 → ((♯‘𝐵)C0) = 1)
5755, 56syl 17 . . . . 5 (𝐵 ∈ Fin → ((♯‘𝐵)C0) = 1)
5857oveq2d 6860 . . . 4 (𝐵 ∈ Fin → (1 · ((♯‘𝐵)C0)) = (1 · 1))
59 1t1e1 11442 . . . 4 (1 · 1) = 1
6058, 59syl6req 2816 . . 3 (𝐵 ∈ Fin → 1 = (1 · ((♯‘𝐵)C0)))
61 abn0 4121 . . . . . . . . . . . . 13 ({𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} ≠ ∅ ↔ ∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1𝐵)
62 f1domg 8182 . . . . . . . . . . . . . . . 16 (𝐵 ∈ Fin → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
6362adantr 472 . . . . . . . . . . . . . . 15 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
64 vex 3353 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
65 hashunsng 13386 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
6664, 65ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
6766adantl 473 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
6867breq1d 4821 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
69 simprl 787 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ∈ Fin)
70 snfi 8247 . . . . . . . . . . . . . . . . . 18 {𝑧} ∈ Fin
71 unfi 8436 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
7269, 70, 71sylancl 580 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin)
73 simpl 474 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝐵 ∈ Fin)
74 hashdom 13373 . . . . . . . . . . . . . . . . 17 (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
7572, 73, 74syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
76 hashcl 13352 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ0)
7776ad2antrl 719 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝑦) ∈ ℕ0)
78 nn0p1nn 11581 . . . . . . . . . . . . . . . . . . 19 ((♯‘𝑦) ∈ ℕ0 → ((♯‘𝑦) + 1) ∈ ℕ)
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝑦) + 1) ∈ ℕ)
8079nnred 11293 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝑦) + 1) ∈ ℝ)
8155adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝐵) ∈ ℕ0)
8281nn0red 11601 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝐵) ∈ ℝ)
8380, 82lenltd 10439 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (((♯‘𝑦) + 1) ≤ (♯‘𝐵) ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8468, 75, 833bitr3d 300 . . . . . . . . . . . . . . 15 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝑦 ∪ {𝑧}) ≼ 𝐵 ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8563, 84sylibd 230 . . . . . . . . . . . . . 14 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8685exlimdv 2028 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8761, 86syl5bi 233 . . . . . . . . . . . 12 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ({𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} ≠ ∅ → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8887necon4ad 2956 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝐵) < ((♯‘𝑦) + 1) → {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} = ∅))
8988imp 395 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} = ∅)
9089fveq2d 6381 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = (♯‘∅))
91 hashcl 13352 . . . . . . . . . . . . . 14 ((𝑦 ∪ {𝑧}) ∈ Fin → (♯‘(𝑦 ∪ {𝑧})) ∈ ℕ0)
9272, 91syl 17 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝑦 ∪ {𝑧})) ∈ ℕ0)
93 faccl 13277 . . . . . . . . . . . . 13 ((♯‘(𝑦 ∪ {𝑧})) ∈ ℕ0 → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
9492, 93syl 17 . . . . . . . . . . . 12 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
9594nncnd 11294 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
9695adantr 472 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
9796mul01d 10491 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0) = 0)
9819, 90, 973eqtr4a 2825 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0))
9967adantr 472 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
10099oveq2d 6860 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1)))
10181adantr 472 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) ∈ ℕ0)
10279adantr 472 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈ ℕ)
103102nnzd 11731 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈ ℤ)
104 simpr 477 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) < ((♯‘𝑦) + 1))
105104olcd 900 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (((♯‘𝑦) + 1) < 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1)))
106 bcval4 13301 . . . . . . . . . . 11 (((♯‘𝐵) ∈ ℕ0 ∧ ((♯‘𝑦) + 1) ∈ ℤ ∧ (((♯‘𝑦) + 1) < 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1))) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0)
107101, 103, 105, 106syl3anc 1490 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0)
108100, 107eqtrd 2799 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = 0)
109108oveq2d 6860 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0))
11098, 109eqtr4d 2802 . . . . . . 7 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))
111110a1d 25 . . . . . 6 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
112 oveq2 6852 . . . . . . 7 ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
11369adantr 472 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝑦 ∈ Fin)
11473adantr 472 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝐵 ∈ Fin)
115 simplrr 796 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ¬ 𝑧𝑦)
116 simpr 477 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ≤ (♯‘𝐵))
117113, 114, 115, 116hashf1lem2 13444 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})))
11881adantr 472 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
119 faccl 13277 . . . . . . . . . . . . . 14 ((♯‘𝐵) ∈ ℕ0 → (!‘(♯‘𝐵)) ∈ ℕ)
120118, 119syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈ ℕ)
121120nncnd 11294 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈ ℂ)
12277adantr 472 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℕ0)
123 peano2nn0 11582 . . . . . . . . . . . . . . . 16 ((♯‘𝑦) ∈ ℕ0 → ((♯‘𝑦) + 1) ∈ ℕ0)
124122, 123syl 17 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ ℕ0)
125 nn0sub2 11688 . . . . . . . . . . . . . . 15 ((((♯‘𝑦) + 1) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ0)
126124, 118, 116, 125syl3anc 1490 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ0)
127 faccl 13277 . . . . . . . . . . . . . 14 (((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ0 → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℕ)
128126, 127syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℕ)
129128nncnd 11294 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℂ)
130128nnne0d 11324 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ≠ 0)
131121, 129, 130divcld 11057 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) ∈ ℂ)
132 faccl 13277 . . . . . . . . . . . . 13 (((♯‘𝑦) + 1) ∈ ℕ0 → (!‘((♯‘𝑦) + 1)) ∈ ℕ)
133124, 132syl 17 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈ ℕ)
134133nncnd 11294 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈ ℂ)
135133nnne0d 11324 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ≠ 0)
136131, 134, 135divcan2d 11059 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))))
137118nn0cnd 11602 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ)
138122nn0cnd 11602 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℂ)
139137, 138subcld 10648 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ)
140 ax-1cn 10249 . . . . . . . . . . . . . 14 1 ∈ ℂ
141 npcan 10546 . . . . . . . . . . . . . 14 ((((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) = ((♯‘𝐵) − (♯‘𝑦)))
142139, 140, 141sylancl 580 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) = ((♯‘𝐵) − (♯‘𝑦)))
143 1cnd 10290 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 1 ∈ ℂ)
144137, 138, 143subsub4d 10679 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) = ((♯‘𝐵) − ((♯‘𝑦) + 1)))
145144, 126eqeltrd 2844 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) ∈ ℕ0)
146 nn0p1nn 11581 . . . . . . . . . . . . . 14 ((((♯‘𝐵) − (♯‘𝑦)) − 1) ∈ ℕ0 → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈ ℕ)
147145, 146syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈ ℕ)
148142, 147eqeltrrd 2845 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ)
149148nnne0d 11324 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ≠ 0)
150131, 139, 149divcan2d 11059 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))))
151136, 150eqtr4d 2802 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))))
15267adantr 472 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
153152fveq2d 6381 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) = (!‘((♯‘𝑦) + 1)))
154 nn0uz 11925 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
155124, 154syl6eleq 2854 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (ℤ‘0))
156118nn0zd 11730 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
157 elfz5 12544 . . . . . . . . . . . . . 14 ((((♯‘𝑦) + 1) ∈ (ℤ‘0) ∧ (♯‘𝐵) ∈ ℤ) → (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
158155, 156, 157syl2anc 579 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
159116, 158mpbird 248 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)))
160 bcval2 13299 . . . . . . . . . . . 12 (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
161159, 160syl 17 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
162152oveq2d 6860 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1)))
163121, 129, 134, 130, 135divdiv1d 11088 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
164161, 162, 1633eqtr4d 2809 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1))))
165153, 164oveq12d 6862 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))))
166122, 154syl6eleq 2854 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (ℤ‘0))
167 peano2fzr 12564 . . . . . . . . . . . . . . 15 (((♯‘𝑦) ∈ (ℤ‘0) ∧ ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵))) → (♯‘𝑦) ∈ (0...(♯‘𝐵)))
168166, 159, 167syl2anc 579 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (0...(♯‘𝐵)))
169 bcval2 13299 . . . . . . . . . . . . . 14 ((♯‘𝑦) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
170168, 169syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
171 elfzle2 12555 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑦) ∈ (0...(♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵))
172168, 171syl 17 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵))
173 nn0sub2 11688 . . . . . . . . . . . . . . . . 17 (((♯‘𝑦) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝑦) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ0)
174122, 118, 172, 173syl3anc 1490 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ0)
175 faccl 13277 . . . . . . . . . . . . . . . 16 (((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ0 → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℕ)
176174, 175syl 17 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℕ)
177176nncnd 11294 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℂ)
178 faccl 13277 . . . . . . . . . . . . . . . 16 ((♯‘𝑦) ∈ ℕ0 → (!‘(♯‘𝑦)) ∈ ℕ)
179122, 178syl 17 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈ ℕ)
180179nncnd 11294 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈ ℂ)
181176nnne0d 11324 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ≠ 0)
182179nnne0d 11324 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ≠ 0)
183121, 177, 180, 181, 182divdiv1d 11088 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
184170, 183eqtr4d 2802 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦))))
185184oveq2d 6860 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) = ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))))
186 facnn2 13276 . . . . . . . . . . . . . . 15 (((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))))
187148, 186syl 17 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))))
188144fveq2d 6381 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) = (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))))
189188oveq1d 6859 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))) = ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))
190187, 189eqtrd 2799 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))
191190oveq2d 6860 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))))
192121, 177, 181divcld 11057 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) ∈ ℂ)
193192, 180, 182divcan2d 11059 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))))
194121, 129, 139, 130, 149divdiv1d 11088 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))))
195191, 193, 1943eqtr4d 2809 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))))
196185, 195eqtrd 2799 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))))
197196oveq2d 6860 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))))
198151, 165, 1973eqtr4d 2809 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
199117, 198eqeq12d 2780 . . . . . . 7 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) ↔ (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))))
200112, 199syl5ibr 237 . . . . . 6 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
201111, 200, 82, 80ltlecasei 10401 . . . . 5 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
202201expcom 402 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝐵 ∈ Fin → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))))
203202a2d 29 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))) → (𝐵 ∈ Fin → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))))
20427, 36, 45, 54, 60, 203findcard2s 8410 . 2 (𝐴 ∈ Fin → (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴)))))
205204imp 395 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wne 2937  Vcvv 3350  cun 3732  c0 4081  {csn 4336   class class class wbr 4811   Fn wfn 6065  1-1wf1 6067  cfv 6070  (class class class)co 6844  cdom 8160  Fincfn 8162  cc 10189  0cc0 10191  1c1 10192   + caddc 10194   · cmul 10196   < clt 10330  cle 10331  cmin 10522   / cdiv 10940  cn 11276  0cn0 11540  cz 11626  cuz 11889  ...cfz 12536  !cfa 13267  Ccbc 13296  chash 13324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-1st 7368  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-er 7949  df-map 8064  df-pm 8065  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-card 9018  df-cda 9245  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-n0 11541  df-xnn0 11613  df-z 11627  df-uz 11890  df-fz 12537  df-seq 13012  df-fac 13268  df-bc 13297  df-hash 13325
This theorem is referenced by:  hashfac  13446  birthdaylem2  24973
  Copyright terms: Public domain W3C validator