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

Theorem hashf1 13443
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 6237 . . . . . . . . 9 (𝑥 = ∅ → (𝑓:𝑥1-1𝐵𝑓:∅–1-1𝐵))
2 f1fn 6242 . . . . . . . . . . . 12 (𝑓:∅–1-1𝐵𝑓 Fn ∅)
3 fn0 6151 . . . . . . . . . . . 12 (𝑓 Fn ∅ ↔ 𝑓 = ∅)
42, 3sylib 208 . . . . . . . . . . 11 (𝑓:∅–1-1𝐵𝑓 = ∅)
5 f10 6310 . . . . . . . . . . . 12 ∅:∅–1-1𝐵
6 f1eq1 6236 . . . . . . . . . . . 12 (𝑓 = ∅ → (𝑓:∅–1-1𝐵 ↔ ∅:∅–1-1𝐵))
75, 6mpbiri 248 . . . . . . . . . . 11 (𝑓 = ∅ → 𝑓:∅–1-1𝐵)
84, 7impbii 199 . . . . . . . . . 10 (𝑓:∅–1-1𝐵𝑓 = ∅)
9 velsn 4332 . . . . . . . . . 10 (𝑓 ∈ {∅} ↔ 𝑓 = ∅)
108, 9bitr4i 267 . . . . . . . . 9 (𝑓:∅–1-1𝐵𝑓 ∈ {∅})
111, 10syl6bb 276 . . . . . . . 8 (𝑥 = ∅ → (𝑓:𝑥1-1𝐵𝑓 ∈ {∅}))
1211abbi1dv 2892 . . . . . . 7 (𝑥 = ∅ → {𝑓𝑓:𝑥1-1𝐵} = {∅})
1312fveq2d 6336 . . . . . 6 (𝑥 = ∅ → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{∅}))
14 0ex 4924 . . . . . . 7 ∅ ∈ V
15 hashsng 13361 . . . . . . 7 (∅ ∈ V → (♯‘{∅}) = 1)
1614, 15ax-mp 5 . . . . . 6 (♯‘{∅}) = 1
1713, 16syl6eq 2821 . . . . 5 (𝑥 = ∅ → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = 1)
18 fveq2 6332 . . . . . . . . 9 (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
19 hash0 13360 . . . . . . . . 9 (♯‘∅) = 0
2018, 19syl6eq 2821 . . . . . . . 8 (𝑥 = ∅ → (♯‘𝑥) = 0)
2120fveq2d 6336 . . . . . . 7 (𝑥 = ∅ → (!‘(♯‘𝑥)) = (!‘0))
22 fac0 13267 . . . . . . 7 (!‘0) = 1
2321, 22syl6eq 2821 . . . . . 6 (𝑥 = ∅ → (!‘(♯‘𝑥)) = 1)
2420oveq2d 6809 . . . . . 6 (𝑥 = ∅ → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C0))
2523, 24oveq12d 6811 . . . . 5 (𝑥 = ∅ → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = (1 · ((♯‘𝐵)C0)))
2617, 25eqeq12d 2786 . . . 4 (𝑥 = ∅ → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ 1 = (1 · ((♯‘𝐵)C0))))
2726imbi2d 329 . . 3 (𝑥 = ∅ → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → 1 = (1 · ((♯‘𝐵)C0)))))
28 f1eq2 6237 . . . . . . 7 (𝑥 = 𝑦 → (𝑓:𝑥1-1𝐵𝑓:𝑦1-1𝐵))
2928abbidv 2890 . . . . . 6 (𝑥 = 𝑦 → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:𝑦1-1𝐵})
3029fveq2d 6336 . . . . 5 (𝑥 = 𝑦 → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:𝑦1-1𝐵}))
31 fveq2 6332 . . . . . . 7 (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
3231fveq2d 6336 . . . . . 6 (𝑥 = 𝑦 → (!‘(♯‘𝑥)) = (!‘(♯‘𝑦)))
3331oveq2d 6809 . . . . . 6 (𝑥 = 𝑦 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝑦)))
3432, 33oveq12d 6811 . . . . 5 (𝑥 = 𝑦 → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))
3530, 34eqeq12d 2786 . . . 4 (𝑥 = 𝑦 → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
3635imbi2d 329 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))))
37 f1eq2 6237 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓:𝑥1-1𝐵𝑓:(𝑦 ∪ {𝑧})–1-1𝐵))
3837abbidv 2890 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵})
3938fveq2d 6336 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}))
40 fveq2 6332 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
4140fveq2d 6336 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (!‘(♯‘𝑥)) = (!‘(♯‘(𝑦 ∪ {𝑧}))))
4240oveq2d 6809 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))
4341, 42oveq12d 6811 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))
4439, 43eqeq12d 2786 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
4544imbi2d 329 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))))
46 f1eq2 6237 . . . . . . 7 (𝑥 = 𝐴 → (𝑓:𝑥1-1𝐵𝑓:𝐴1-1𝐵))
4746abbidv 2890 . . . . . 6 (𝑥 = 𝐴 → {𝑓𝑓:𝑥1-1𝐵} = {𝑓𝑓:𝐴1-1𝐵})
4847fveq2d 6336 . . . . 5 (𝑥 = 𝐴 → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = (♯‘{𝑓𝑓:𝐴1-1𝐵}))
49 fveq2 6332 . . . . . . 7 (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴))
5049fveq2d 6336 . . . . . 6 (𝑥 = 𝐴 → (!‘(♯‘𝑥)) = (!‘(♯‘𝐴)))
5149oveq2d 6809 . . . . . 6 (𝑥 = 𝐴 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝐴)))
5250, 51oveq12d 6811 . . . . 5 (𝑥 = 𝐴 → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))
5348, 52eqeq12d 2786 . . . 4 (𝑥 = 𝐴 → ((♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴)))))
5453imbi2d 329 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝑥1-1𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))))
55 hashcl 13349 . . . . . 6 (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
56 bcn0 13301 . . . . . 6 ((♯‘𝐵) ∈ ℕ0 → ((♯‘𝐵)C0) = 1)
5755, 56syl 17 . . . . 5 (𝐵 ∈ Fin → ((♯‘𝐵)C0) = 1)
5857oveq2d 6809 . . . 4 (𝐵 ∈ Fin → (1 · ((♯‘𝐵)C0)) = (1 · 1))
59 1t1e1 11377 . . . 4 (1 · 1) = 1
6058, 59syl6req 2822 . . 3 (𝐵 ∈ Fin → 1 = (1 · ((♯‘𝐵)C0)))
61 abn0 4101 . . . . . . . . . . . . 13 ({𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} ≠ ∅ ↔ ∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1𝐵)
62 f1domg 8129 . . . . . . . . . . . . . . . 16 (𝐵 ∈ Fin → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
6362adantr 466 . . . . . . . . . . . . . . 15 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
64 vex 3354 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
65 hashunsng 13383 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
6664, 65ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
6766adantl 467 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
6867breq1d 4796 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
69 simprl 746 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ∈ Fin)
70 snfi 8194 . . . . . . . . . . . . . . . . . 18 {𝑧} ∈ Fin
71 unfi 8383 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
7269, 70, 71sylancl 566 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin)
73 simpl 468 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝐵 ∈ Fin)
74 hashdom 13370 . . . . . . . . . . . . . . . . 17 (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
7572, 73, 74syl2anc 565 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
76 hashcl 13349 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ0)
7776ad2antrl 699 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝑦) ∈ ℕ0)
78 nn0p1nn 11534 . . . . . . . . . . . . . . . . . . 19 ((♯‘𝑦) ∈ ℕ0 → ((♯‘𝑦) + 1) ∈ ℕ)
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝑦) + 1) ∈ ℕ)
8079nnred 11237 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝑦) + 1) ∈ ℝ)
8155adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝐵) ∈ ℕ0)
8281nn0red 11554 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘𝐵) ∈ ℝ)
8380, 82lenltd 10385 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (((♯‘𝑦) + 1) ≤ (♯‘𝐵) ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8468, 75, 833bitr3d 298 . . . . . . . . . . . . . . 15 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝑦 ∪ {𝑧}) ≼ 𝐵 ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8563, 84sylibd 229 . . . . . . . . . . . . . 14 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8685exlimdv 2013 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8761, 86syl5bi 232 . . . . . . . . . . . 12 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ({𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} ≠ ∅ → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
8887necon4ad 2962 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘𝐵) < ((♯‘𝑦) + 1) → {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} = ∅))
8988imp 393 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → {𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵} = ∅)
9089fveq2d 6336 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = (♯‘∅))
91 hashcl 13349 . . . . . . . . . . . . . 14 ((𝑦 ∪ {𝑧}) ∈ Fin → (♯‘(𝑦 ∪ {𝑧})) ∈ ℕ0)
9272, 91syl 17 . . . . . . . . . . . . 13 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (♯‘(𝑦 ∪ {𝑧})) ∈ ℕ0)
93 faccl 13274 . . . . . . . . . . . . 13 ((♯‘(𝑦 ∪ {𝑧})) ∈ ℕ0 → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
9492, 93syl 17 . . . . . . . . . . . 12 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
9594nncnd 11238 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
9695adantr 466 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
9796mul01d 10437 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0) = 0)
9819, 90, 973eqtr4a 2831 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0))
9967adantr 466 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
10099oveq2d 6809 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1)))
10181adantr 466 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) ∈ ℕ0)
10279adantr 466 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈ ℕ)
103102nnzd 11683 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈ ℤ)
104 simpr 471 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) < ((♯‘𝑦) + 1))
105104olcd 853 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (((♯‘𝑦) + 1) < 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1)))
106 bcval4 13298 . . . . . . . . . . 11 (((♯‘𝐵) ∈ ℕ0 ∧ ((♯‘𝑦) + 1) ∈ ℤ ∧ (((♯‘𝑦) + 1) < 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1))) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0)
107101, 103, 105, 106syl3anc 1476 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0)
108100, 107eqtrd 2805 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = 0)
109108oveq2d 6809 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0))
11098, 109eqtr4d 2808 . . . . . . 7 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))
111110a1d 25 . . . . . 6 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
112 oveq2 6801 . . . . . . 7 ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
11369adantr 466 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝑦 ∈ Fin)
11473adantr 466 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝐵 ∈ Fin)
115 simplrr 755 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ¬ 𝑧𝑦)
116 simpr 471 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ≤ (♯‘𝐵))
117113, 114, 115, 116hashf1lem2 13442 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})))
11881adantr 466 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
119 faccl 13274 . . . . . . . . . . . . . 14 ((♯‘𝐵) ∈ ℕ0 → (!‘(♯‘𝐵)) ∈ ℕ)
120118, 119syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈ ℕ)
121120nncnd 11238 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈ ℂ)
12277adantr 466 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℕ0)
123 peano2nn0 11535 . . . . . . . . . . . . . . . 16 ((♯‘𝑦) ∈ ℕ0 → ((♯‘𝑦) + 1) ∈ ℕ0)
124122, 123syl 17 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ ℕ0)
125 nn0sub2 11640 . . . . . . . . . . . . . . 15 ((((♯‘𝑦) + 1) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ0)
126124, 118, 116, 125syl3anc 1476 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ0)
127 faccl 13274 . . . . . . . . . . . . . 14 (((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ0 → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℕ)
128126, 127syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℕ)
129128nncnd 11238 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℂ)
130128nnne0d 11267 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ≠ 0)
131121, 129, 130divcld 11003 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) ∈ ℂ)
132 faccl 13274 . . . . . . . . . . . . 13 (((♯‘𝑦) + 1) ∈ ℕ0 → (!‘((♯‘𝑦) + 1)) ∈ ℕ)
133124, 132syl 17 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈ ℕ)
134133nncnd 11238 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈ ℂ)
135133nnne0d 11267 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ≠ 0)
136131, 134, 135divcan2d 11005 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))))
137118nn0cnd 11555 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ)
138122nn0cnd 11555 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℂ)
139137, 138subcld 10594 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ)
140 ax-1cn 10196 . . . . . . . . . . . . . 14 1 ∈ ℂ
141 npcan 10492 . . . . . . . . . . . . . 14 ((((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) = ((♯‘𝐵) − (♯‘𝑦)))
142139, 140, 141sylancl 566 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) = ((♯‘𝐵) − (♯‘𝑦)))
143 1cnd 10258 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 1 ∈ ℂ)
144137, 138, 143subsub4d 10625 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) = ((♯‘𝐵) − ((♯‘𝑦) + 1)))
145144, 126eqeltrd 2850 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) ∈ ℕ0)
146 nn0p1nn 11534 . . . . . . . . . . . . . 14 ((((♯‘𝐵) − (♯‘𝑦)) − 1) ∈ ℕ0 → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈ ℕ)
147145, 146syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈ ℕ)
148142, 147eqeltrrd 2851 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ)
149148nnne0d 11267 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ≠ 0)
150131, 139, 149divcan2d 11005 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))))
151136, 150eqtr4d 2808 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))))
15267adantr 466 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
153152fveq2d 6336 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) = (!‘((♯‘𝑦) + 1)))
154 nn0uz 11924 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
155124, 154syl6eleq 2860 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (ℤ‘0))
156118nn0zd 11682 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
157 elfz5 12541 . . . . . . . . . . . . . 14 ((((♯‘𝑦) + 1) ∈ (ℤ‘0) ∧ (♯‘𝐵) ∈ ℤ) → (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
158155, 156, 157syl2anc 565 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
159116, 158mpbird 247 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)))
160 bcval2 13296 . . . . . . . . . . . 12 (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
161159, 160syl 17 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
162152oveq2d 6809 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1)))
163121, 129, 134, 130, 135divdiv1d 11034 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
164161, 162, 1633eqtr4d 2815 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1))))
165153, 164oveq12d 6811 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))))
166122, 154syl6eleq 2860 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (ℤ‘0))
167 peano2fzr 12561 . . . . . . . . . . . . . . 15 (((♯‘𝑦) ∈ (ℤ‘0) ∧ ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵))) → (♯‘𝑦) ∈ (0...(♯‘𝐵)))
168166, 159, 167syl2anc 565 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (0...(♯‘𝐵)))
169 bcval2 13296 . . . . . . . . . . . . . 14 ((♯‘𝑦) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
170168, 169syl 17 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
171 elfzle2 12552 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑦) ∈ (0...(♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵))
172168, 171syl 17 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵))
173 nn0sub2 11640 . . . . . . . . . . . . . . . . 17 (((♯‘𝑦) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝑦) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ0)
174122, 118, 172, 173syl3anc 1476 . . . . . . . . . . . . . . . 16 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ0)
175 faccl 13274 . . . . . . . . . . . . . . . 16 (((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ0 → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℕ)
176174, 175syl 17 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℕ)
177176nncnd 11238 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℂ)
178 faccl 13274 . . . . . . . . . . . . . . . 16 ((♯‘𝑦) ∈ ℕ0 → (!‘(♯‘𝑦)) ∈ ℕ)
179122, 178syl 17 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈ ℕ)
180179nncnd 11238 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈ ℂ)
181176nnne0d 11267 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ≠ 0)
182179nnne0d 11267 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ≠ 0)
183121, 177, 180, 181, 182divdiv1d 11034 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
184170, 183eqtr4d 2808 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦))))
185184oveq2d 6809 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) = ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))))
186 facnn2 13273 . . . . . . . . . . . . . . 15 (((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))))
187148, 186syl 17 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))))
188144fveq2d 6336 . . . . . . . . . . . . . . 15 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) = (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))))
189188oveq1d 6808 . . . . . . . . . . . . . 14 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))) = ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))
190187, 189eqtrd 2805 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))
191190oveq2d 6809 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))))
192121, 177, 181divcld 11003 . . . . . . . . . . . . 13 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) ∈ ℂ)
193192, 180, 182divcan2d 11005 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))))
194121, 129, 139, 130, 149divdiv1d 11034 . . . . . . . . . . . 12 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))))
195191, 193, 1943eqtr4d 2815 . . . . . . . . . . 11 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))))
196185, 195eqtrd 2805 . . . . . . . . . 10 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))))
197196oveq2d 6809 . . . . . . . . 9 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))))
198151, 165, 1973eqtr4d 2815 . . . . . . . 8 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
199117, 198eqeq12d 2786 . . . . . . 7 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) ↔ (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓𝑓:𝑦1-1𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))))
200112, 199syl5ibr 236 . . . . . 6 (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
201111, 200, 82, 80ltlecasei 10347 . . . . 5 ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((♯‘{𝑓𝑓:𝑦1-1𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓𝑓:(𝑦 ∪ {𝑧})–1-1𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
202201expcom 398 . . . 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 8357 . 2 (𝐴 ∈ Fin → (𝐵 ∈ Fin → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴)))))
205204imp 393 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘{𝑓𝑓:𝐴1-1𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 826   = wceq 1631  wex 1852  wcel 2145  {cab 2757  wne 2943  Vcvv 3351  cun 3721  c0 4063  {csn 4316   class class class wbr 4786   Fn wfn 6026  1-1wf1 6028  cfv 6031  (class class class)co 6793  cdom 8107  Fincfn 8109  cc 10136  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143   < clt 10276  cle 10277  cmin 10468   / cdiv 10886  cn 11222  0cn0 11494  cz 11579  cuz 11888  ...cfz 12533  !cfa 13264  Ccbc 13293  chash 13321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-n0 11495  df-xnn0 11566  df-z 11580  df-uz 11889  df-fz 12534  df-seq 13009  df-fac 13265  df-bc 13294  df-hash 13322
This theorem is referenced by:  hashfac  13444  birthdaylem2  24900
  Copyright terms: Public domain W3C validator