This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashf1

Description: The permutation number | A | ! x. ( | B | _C | A | ) = | B | ! / ( | B | - | A | ) ! counts the number of injections from A to B . (Contributed by Mario Carneiro, 21-Jan-2015)

Ref Expression
Assertion hashf1 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 f1eq2 ⊢ ( 𝑥 = ∅ → ( 𝑓 : 𝑥 –1-1→ 𝐵 ↔ 𝑓 : ∅ –1-1→ 𝐵 ) )
2 f1fn ⊢ ( 𝑓 : ∅ –1-1→ 𝐵 → 𝑓 Fn ∅ )
3 fn0 ⊢ ( 𝑓 Fn ∅ ↔ 𝑓 = ∅ )
4 2 3 sylib ⊢ ( 𝑓 : ∅ –1-1→ 𝐵 → 𝑓 = ∅ )
5 f10 ⊢ ∅ : ∅ –1-1→ 𝐵
6 f1eq1 ⊢ ( 𝑓 = ∅ → ( 𝑓 : ∅ –1-1→ 𝐵 ↔ ∅ : ∅ –1-1→ 𝐵 ) )
7 5 6 mpbiri ⊢ ( 𝑓 = ∅ → 𝑓 : ∅ –1-1→ 𝐵 )
8 4 7 impbii ⊢ ( 𝑓 : ∅ –1-1→ 𝐵 ↔ 𝑓 = ∅ )
9 velsn ⊢ ( 𝑓 ∈ { ∅ } ↔ 𝑓 = ∅ )
10 8 9 bitr4i ⊢ ( 𝑓 : ∅ –1-1→ 𝐵 ↔ 𝑓 ∈ { ∅ } )
11 1 10 bitrdi ⊢ ( 𝑥 = ∅ → ( 𝑓 : 𝑥 –1-1→ 𝐵 ↔ 𝑓 ∈ { ∅ } ) )
12 11 eqabcdv ⊢ ( 𝑥 = ∅ → { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } = { ∅ } )
13 12 fveq2d ⊢ ( 𝑥 = ∅ → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ♯ ‘ { ∅ } ) )
14 0ex ⊢ ∅ ∈ V
15 hashsng ⊢ ( ∅ ∈ V → ( ♯ ‘ { ∅ } ) = 1 )
16 14 15 ax-mp ⊢ ( ♯ ‘ { ∅ } ) = 1
17 13 16 eqtrdi ⊢ ( 𝑥 = ∅ → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = 1 )
18 fveq2 ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ∅ ) )
19 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
20 18 19 eqtrdi ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = 0 )
21 20 fveq2d ⊢ ( 𝑥 = ∅ → ( ! ‘ ( ♯ ‘ 𝑥 ) ) = ( ! ‘ 0 ) )
22 fac0 ⊢ ( ! ‘ 0 ) = 1
23 21 22 eqtrdi ⊢ ( 𝑥 = ∅ → ( ! ‘ ( ♯ ‘ 𝑥 ) ) = 1 )
24 20 oveq2d ⊢ ( 𝑥 = ∅ → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) = ( ( ♯ ‘ 𝐵 ) C 0 ) )
25 23 24 oveq12d ⊢ ( 𝑥 = ∅ → ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) = ( 1 · ( ( ♯ ‘ 𝐵 ) C 0 ) ) )
26 17 25 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) ↔ 1 = ( 1 · ( ( ♯ ‘ 𝐵 ) C 0 ) ) ) )
27 26 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝐵 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) ) ↔ ( 𝐵 ∈ Fin → 1 = ( 1 · ( ( ♯ ‘ 𝐵 ) C 0 ) ) ) ) )
28 f1eq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑓 : 𝑥 –1-1→ 𝐵 ↔ 𝑓 : 𝑦 –1-1→ 𝐵 ) )
29 28 abbidv ⊢ ( 𝑥 = 𝑦 → { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } = { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } )
30 29 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) )
31 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( ! ‘ ( ♯ ‘ 𝑥 ) ) = ( ! ‘ ( ♯ ‘ 𝑦 ) ) )
32 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
33 32 oveq2d ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) = ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) )
34 31 33 oveq12d ⊢ ( 𝑥 = 𝑦 → ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) )
35 30 34 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) ↔ ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) ) )
36 35 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) ) ↔ ( 𝐵 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) ) ) )
37 f1eq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑓 : 𝑥 –1-1→ 𝐵 ↔ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 ) )
38 37 abbidv ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } = { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } )
39 38 fveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) )
40 2fveq3 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ! ‘ ( ♯ ‘ 𝑥 ) ) = ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) )
41 fveq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) )
42 41 oveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) = ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) )
43 40 42 oveq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) )
44 39 43 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) ↔ ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
45 44 imbi2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐵 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) ) ↔ ( 𝐵 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) ) )
46 f1eq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑓 : 𝑥 –1-1→ 𝐵 ↔ 𝑓 : 𝐴 –1-1→ 𝐵 ) )
47 46 abbidv ⊢ ( 𝑥 = 𝐴 → { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } = { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } )
48 47 fveq2d ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ) )
49 2fveq3 ⊢ ( 𝑥 = 𝐴 → ( ! ‘ ( ♯ ‘ 𝑥 ) ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )
50 fveq2 ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) )
51 50 oveq2d ⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) = ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝐴 ) ) )
52 49 51 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝐴 ) ) ) )
53 48 52 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) ↔ ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝐴 ) ) ) ) )
54 53 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑥 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑥 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑥 ) ) ) ) ↔ ( 𝐵 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝐴 ) ) ) ) ) )
55 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
56 bcn0 ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐵 ) C 0 ) = 1 )
57 55 56 syl ⊢ ( 𝐵 ∈ Fin → ( ( ♯ ‘ 𝐵 ) C 0 ) = 1 )
58 57 oveq2d ⊢ ( 𝐵 ∈ Fin → ( 1 · ( ( ♯ ‘ 𝐵 ) C 0 ) ) = ( 1 · 1 ) )
59 1t1e1 ⊢ ( 1 · 1 ) = 1
60 58 59 eqtr2di ⊢ ( 𝐵 ∈ Fin → 1 = ( 1 · ( ( ♯ ‘ 𝐵 ) C 0 ) ) )
61 abn0 ⊢ ( { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ≠ ∅ ↔ ∃ 𝑓 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 )
62 f1domg ⊢ ( 𝐵 ∈ Fin → ( 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 → ( 𝑦 ∪ { 𝑧 } ) ≼ 𝐵 ) )
63 62 adantr ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 → ( 𝑦 ∪ { 𝑧 } ) ≼ 𝐵 ) )
64 hashunsng ⊢ ( 𝑧 ∈ V → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
65 64 elv ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) )
66 65 adantl ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) )
67 66 breq1d ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ≤ ( ♯ ‘ 𝐵 ) ↔ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) )
68 simprl ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝑦 ∈ Fin )
69 snfi ⊢ { 𝑧 } ∈ Fin
70 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
71 68 69 70 sylancl ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
72 simpl ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → 𝐵 ∈ Fin )
73 hashdom ⊢ ( ( ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ≤ ( ♯ ‘ 𝐵 ) ↔ ( 𝑦 ∪ { 𝑧 } ) ≼ 𝐵 ) )
74 71 72 73 syl2anc ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ≤ ( ♯ ‘ 𝐵 ) ↔ ( 𝑦 ∪ { 𝑧 } ) ≼ 𝐵 ) )
75 hashcl ⊢ ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
76 75 ad2antrl ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
77 nn0p1nn ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ℕ )
78 76 77 syl ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ℕ )
79 78 nnred ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ℝ )
80 55 adantr ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
81 80 nn0red ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
82 79 81 lenltd ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ↔ ¬ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
83 67 74 82 3bitr3d ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ≼ 𝐵 ↔ ¬ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
84 63 83 sylibd ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 → ¬ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
85 84 exlimdv ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ∃ 𝑓 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 → ¬ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
86 61 85 biimtrid ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ≠ ∅ → ¬ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
87 86 necon4ad ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) → { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } = ∅ ) )
88 87 imp ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } = ∅ )
89 88 fveq2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ♯ ‘ ∅ ) )
90 hashcl ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ∈ Fin → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ0 )
91 71 90 syl ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ∈ ℕ0 )
92 91 faccld ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ ℕ )
93 92 nncnd ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ ℂ )
94 93 adantr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ ℂ )
95 94 mul01d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · 0 ) = 0 )
96 19 89 95 3eqtr4a ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · 0 ) )
97 66 adantr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) )
98 97 oveq2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ♯ ‘ 𝐵 ) C ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
99 80 adantr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
100 78 adantr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ℕ )
101 100 nnzd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ℤ )
102 animorr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ( ( ♯ ‘ 𝑦 ) + 1 ) < 0 ∨ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
103 bcval4 ⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ℤ ∧ ( ( ( ♯ ‘ 𝑦 ) + 1 ) < 0 ∨ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) → ( ( ♯ ‘ 𝐵 ) C ( ( ♯ ‘ 𝑦 ) + 1 ) ) = 0 )
104 99 101 102 103 syl3anc ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ( ♯ ‘ 𝐵 ) C ( ( ♯ ‘ 𝑦 ) + 1 ) ) = 0 )
105 98 104 eqtrd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = 0 )
106 105 oveq2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · 0 ) )
107 96 106 eqtr4d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) )
108 107 a1d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ♯ ‘ 𝐵 ) < ( ( ♯ ‘ 𝑦 ) + 1 ) ) → ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
109 oveq2 ⊢ ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) → ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) · ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) ) = ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) · ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) ) )
110 68 adantr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → 𝑦 ∈ Fin )
111 72 adantr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → 𝐵 ∈ Fin )
112 simplrr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ¬ 𝑧 ∈ 𝑦 )
113 simpr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) )
114 110 111 112 113 hashf1lem2 ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) · ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) ) )
115 80 adantr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
116 115 faccld ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ♯ ‘ 𝐵 ) ) ∈ ℕ )
117 116 nncnd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ♯ ‘ 𝐵 ) ) ∈ ℂ )
118 76 adantr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
119 peano2nn0 ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ℕ0 )
120 118 119 syl ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ℕ0 )
121 nn0sub2 ⊢ ( ( ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ∈ ℕ0 )
122 120 115 113 121 syl3anc ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ∈ ℕ0 )
123 122 faccld ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ∈ ℕ )
124 123 nncnd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ∈ ℂ )
125 123 nnne0d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ≠ 0 )
126 117 124 125 divcld ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) ∈ ℂ )
127 120 faccld ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ∈ ℕ )
128 127 nncnd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ∈ ℂ )
129 127 nnne0d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ≠ 0 )
130 126 128 129 divcan2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) · ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) )
131 115 nn0cnd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℂ )
132 118 nn0cnd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝑦 ) ∈ ℂ )
133 131 132 subcld ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ∈ ℂ )
134 ax-1cn ⊢ 1 ∈ ℂ
135 npcan ⊢ ( ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) + 1 ) = ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) )
136 133 134 135 sylancl ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) + 1 ) = ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) )
137 1cnd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → 1 ∈ ℂ )
138 131 132 137 subsub4d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) = ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
139 138 122 eqeltrd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) ∈ ℕ0 )
140 nn0p1nn ⊢ ( ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) ∈ ℕ0 → ( ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) + 1 ) ∈ ℕ )
141 139 140 syl ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) + 1 ) ∈ ℕ )
142 136 141 eqeltrrd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ∈ ℕ )
143 142 nnne0d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ≠ 0 )
144 126 133 143 divcan2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) · ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) )
145 130 144 eqtr4d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) · ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) = ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) · ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) )
146 66 adantr ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) )
147 146 fveq2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
148 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
149 120 148 eleqtrdi ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
150 115 nn0zd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
151 elfz5 ⊢ ( ( ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) → ( ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ↔ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) )
152 149 150 151 syl2anc ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ↔ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) )
153 113 152 mpbird ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) )
154 bcval2 ⊢ ( ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) C ( ( ♯ ‘ 𝑦 ) + 1 ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) · ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) )
155 153 154 syl ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) C ( ( ♯ ‘ 𝑦 ) + 1 ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) · ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) )
156 146 oveq2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ♯ ‘ 𝐵 ) C ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
157 117 124 128 125 129 divdiv1d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) · ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) )
158 155 156 157 3eqtr4d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) )
159 147 158 oveq12d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) · ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ! ‘ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) )
160 118 148 eleqtrdi ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 0 ) )
161 peano2fzr ⊢ ( ( ( ♯ ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝑦 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) )
162 160 153 161 syl2anc ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝑦 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) )
163 bcval2 ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) · ( ! ‘ ( ♯ ‘ 𝑦 ) ) ) ) )
164 162 163 syl ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) · ( ! ‘ ( ♯ ‘ 𝑦 ) ) ) ) )
165 elfzle2 ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝑦 ) ≤ ( ♯ ‘ 𝐵 ) )
166 162 165 syl ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝑦 ) ≤ ( ♯ ‘ 𝐵 ) )
167 nn0sub2 ⊢ ( ( ( ♯ ‘ 𝑦 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ∈ ℕ0 )
168 118 115 166 167 syl3anc ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ∈ ℕ0 )
169 168 faccld ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ∈ ℕ )
170 169 nncnd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ∈ ℂ )
171 118 faccld ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ♯ ‘ 𝑦 ) ) ∈ ℕ )
172 171 nncnd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ♯ ‘ 𝑦 ) ) ∈ ℂ )
173 169 nnne0d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ≠ 0 )
174 171 nnne0d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ♯ ‘ 𝑦 ) ) ≠ 0 )
175 117 170 172 173 174 divdiv1d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) / ( ! ‘ ( ♯ ‘ 𝑦 ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) · ( ! ‘ ( ♯ ‘ 𝑦 ) ) ) ) )
176 164 175 eqtr4d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) = ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) / ( ! ‘ ( ♯ ‘ 𝑦 ) ) ) )
177 176 oveq2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) / ( ! ‘ ( ♯ ‘ 𝑦 ) ) ) ) )
178 facnn2 ⊢ ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ∈ ℕ → ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) = ( ( ! ‘ ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) ) · ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) )
179 142 178 syl ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) = ( ( ! ‘ ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) ) · ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) )
180 138 fveq2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) ) = ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) )
181 180 oveq1d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) − 1 ) ) · ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) = ( ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) · ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) )
182 179 181 eqtrd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) = ( ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) · ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) )
183 182 oveq2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) · ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) )
184 117 170 173 divcld ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) ∈ ℂ )
185 184 172 174 divcan2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) / ( ! ‘ ( ♯ ‘ 𝑦 ) ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) )
186 117 124 133 125 143 divdiv1d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) = ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) · ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) )
187 183 185 186 3eqtr4d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) / ( ! ‘ ( ♯ ‘ 𝑦 ) ) ) ) = ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) )
188 177 187 eqtrd ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) = ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) )
189 188 oveq2d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) · ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) ) = ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) · ( ( ( ! ‘ ( ♯ ‘ 𝐵 ) ) / ( ! ‘ ( ( ♯ ‘ 𝐵 ) − ( ( ♯ ‘ 𝑦 ) + 1 ) ) ) ) / ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) ) ) )
190 145 159 189 3eqtr4d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) · ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) ) )
191 114 190 eqeq12d ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ↔ ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) · ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) ) = ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝑦 ) ) · ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) ) ) )
192 109 191 imbitrrid ⊢ ( ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) ∧ ( ( ♯ ‘ 𝑦 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
193 108 192 81 79 ltlecasei ⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ) → ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) )
194 193 expcom ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( 𝐵 ∈ Fin → ( ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) ) )
195 194 a2d ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝐵 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝑦 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝑦 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝑦 ) ) ) ) → ( 𝐵 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝑦 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) ) ) ) ) )
196 27 36 45 54 60 195 findcard2s ⊢ ( 𝐴 ∈ Fin → ( 𝐵 ∈ Fin → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝐴 ) ) ) ) )
197 196 imp ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ) = ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) · ( ( ♯ ‘ 𝐵 ) C ( ♯ ‘ 𝐴 ) ) ) )