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 ( ♯ ‘ 𝐴 ) ) ) )