hashf1 - Metamath Proof Explorer

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

Theorem hashf1 13098

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.

Step	Hyp	Ref	Expression
1		f1eq2 6010	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:∅–1-1→𝐵))
2		f1fn 6015	. . . . . . . . . . . 12 ⊢ (𝑓:∅–1-1→𝐵 → 𝑓 Fn ∅)
3		fn0 5924	. . . . . . . . . . . 12 ⊢ (𝑓 Fn ∅ ↔ 𝑓 = ∅)
4	2, 3	sylib 207	. . . . . . . . . . 11 ⊢ (𝑓:∅–1-1→𝐵 → 𝑓 = ∅)
5		f10 6081	. . . . . . . . . . . 12 ⊢ ∅:∅–1-1→𝐵
6		f1eq1 6009	. . . . . . . . . . . 12 ⊢ (𝑓 = ∅ → (𝑓:∅–1-1→𝐵 ↔ ∅:∅–1-1→𝐵))
7	5, 6	mpbiri 247	. . . . . . . . . . 11 ⊢ (𝑓 = ∅ → 𝑓:∅–1-1→𝐵)
8	4, 7	impbii 198	. . . . . . . . . 10 ⊢ (𝑓:∅–1-1→𝐵 ↔ 𝑓 = ∅)
9		velsn 4141	. . . . . . . . . 10 ⊢ (𝑓 ∈ {∅} ↔ 𝑓 = ∅)
10	8, 9	bitr4i 266	. . . . . . . . 9 ⊢ (𝑓:∅–1-1→𝐵 ↔ 𝑓 ∈ {∅})
11	1, 10	syl6bb 275	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓 ∈ {∅}))
12	11	abbi1dv 2730	. . . . . . 7 ⊢ (𝑥 = ∅ → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {∅})
13	12	fveq2d 6107	. . . . . 6 ⊢ (𝑥 = ∅ → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (#‘{∅}))
14		0ex 4718	. . . . . . 7 ⊢ ∅ ∈ V
15		hashsng 13020	. . . . . . 7 ⊢ (∅ ∈ V → (#‘{∅}) = 1)
16	14, 15	ax-mp 5	. . . . . 6 ⊢ (#‘{∅}) = 1
17	13, 16	syl6eq 2660	. . . . 5 ⊢ (𝑥 = ∅ → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = 1)
18		fveq2 6103	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (#‘𝑥) = (#‘∅))
19		hash0 13019	. . . . . . . . 9 ⊢ (#‘∅) = 0
20	18, 19	syl6eq 2660	. . . . . . . 8 ⊢ (𝑥 = ∅ → (#‘𝑥) = 0)
21	20	fveq2d 6107	. . . . . . 7 ⊢ (𝑥 = ∅ → (!‘(#‘𝑥)) = (!‘0))
22		fac0 12925	. . . . . . 7 ⊢ (!‘0) = 1
23	21, 22	syl6eq 2660	. . . . . 6 ⊢ (𝑥 = ∅ → (!‘(#‘𝑥)) = 1)
24	20	oveq2d 6565	. . . . . 6 ⊢ (𝑥 = ∅ → ((#‘𝐵)C(#‘𝑥)) = ((#‘𝐵)C0))
25	23, 24	oveq12d 6567	. . . . 5 ⊢ (𝑥 = ∅ → ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) = (1 · ((#‘𝐵)C0)))
26	17, 25	eqeq12d 2625	. . . 4 ⊢ (𝑥 = ∅ → ((#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) ↔ 1 = (1 · ((#‘𝐵)C0))))
27	26	imbi2d 329	. . 3 ⊢ (𝑥 = ∅ → ((𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥)))) ↔ (𝐵 ∈ Fin → 1 = (1 · ((#‘𝐵)C0)))))
28		f1eq2 6010	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:𝑦–1-1→𝐵))
29	28	abbidv 2728	. . . . . 6 ⊢ (𝑥 = 𝑦 → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:𝑦–1-1→𝐵})
30	29	fveq2d 6107	. . . . 5 ⊢ (𝑥 = 𝑦 → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}))
31		fveq2 6103	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦))
32	31	fveq2d 6107	. . . . . 6 ⊢ (𝑥 = 𝑦 → (!‘(#‘𝑥)) = (!‘(#‘𝑦)))
33	31	oveq2d 6565	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((#‘𝐵)C(#‘𝑥)) = ((#‘𝐵)C(#‘𝑦)))
34	32, 33	oveq12d 6567	. . . . 5 ⊢ (𝑥 = 𝑦 → ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))))
35	30, 34	eqeq12d 2625	. . . 4 ⊢ (𝑥 = 𝑦 → ((#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) ↔ (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦)))))
36	35	imbi2d 329	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥)))) ↔ (𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))))))
37		f1eq2 6010	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵))
38	37	abbidv 2728	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵})
39	38	fveq2d 6107	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}))
40		fveq2 6103	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑦 ∪ {𝑧})))
41	40	fveq2d 6107	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (!‘(#‘𝑥)) = (!‘(#‘(𝑦 ∪ {𝑧}))))
42	40	oveq2d 6565	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘𝐵)C(#‘𝑥)) = ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))))
43	41, 42	oveq12d 6567	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))))
44	39, 43	eqeq12d 2625	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) ↔ (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))))))
45	44	imbi2d 329	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥)))) ↔ (𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))))))
46		f1eq2 6010	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:𝐴–1-1→𝐵))
47	46	abbidv 2728	. . . . . 6 ⊢ (𝑥 = 𝐴 → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})
48	47	fveq2d 6107	. . . . 5 ⊢ (𝑥 = 𝐴 → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))
49		fveq2 6103	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (#‘𝑥) = (#‘𝐴))
50	49	fveq2d 6107	. . . . . 6 ⊢ (𝑥 = 𝐴 → (!‘(#‘𝑥)) = (!‘(#‘𝐴)))
51	49	oveq2d 6565	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((#‘𝐵)C(#‘𝑥)) = ((#‘𝐵)C(#‘𝐴)))
52	50, 51	oveq12d 6567	. . . . 5 ⊢ (𝑥 = 𝐴 → ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴))))
53	48, 52	eqeq12d 2625	. . . 4 ⊢ (𝑥 = 𝐴 → ((#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) ↔ (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴)))))
54	53	imbi2d 329	. . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥)))) ↔ (𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴))))))
55		hashcl 13009	. . . . . 6 ⊢ (𝐵 ∈ Fin → (#‘𝐵) ∈ ℕ₀)
56		bcn0 12959	. . . . . 6 ⊢ ((#‘𝐵) ∈ ℕ₀ → ((#‘𝐵)C0) = 1)
57	55, 56	syl 17	. . . . 5 ⊢ (𝐵 ∈ Fin → ((#‘𝐵)C0) = 1)
58	57	oveq2d 6565	. . . 4 ⊢ (𝐵 ∈ Fin → (1 · ((#‘𝐵)C0)) = (1 · 1))
59		1t1e1 11052	. . . 4 ⊢ (1 · 1) = 1
60	58, 59	syl6req 2661	. . 3 ⊢ (𝐵 ∈ Fin → 1 = (1 · ((#‘𝐵)C0)))
61		abn0 3908	. . . . . . . . . . . . 13 ⊢ ({𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} ≠ ∅ ↔ ∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵)
62		f1domg 7861	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
63	62	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
64		vex 3176	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑧 ∈ V
65		hashunsng 13042	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1)))
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))
67	66	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))
68	67	breq1d 4593	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘(𝑦 ∪ {𝑧})) ≤ (#‘𝐵) ↔ ((#‘𝑦) + 1) ≤ (#‘𝐵)))
69		simprl 790	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin)
70		snfi 7923	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ∈ Fin
71		unfi 8112	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
72	69, 70, 71	sylancl 693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin)
73		simpl 472	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐵 ∈ Fin)
74		hashdom 13029	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘(𝑦 ∪ {𝑧})) ≤ (#‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
75	72, 73, 74	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘(𝑦 ∪ {𝑧})) ≤ (#‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
76		hashcl 13009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ Fin → (#‘𝑦) ∈ ℕ₀)
77	76	ad2antrl 760	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘𝑦) ∈ ℕ₀)
78		nn0p1nn 11209	. . . . . . . . . . . . . . . . . . 19 ⊢ ((#‘𝑦) ∈ ℕ₀ → ((#‘𝑦) + 1) ∈ ℕ)
79	77, 78	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘𝑦) + 1) ∈ ℕ)
80	79	nnred 10912	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘𝑦) + 1) ∈ ℝ)
81	55	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘𝐵) ∈ ℕ₀)
82	81	nn0red 11229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘𝐵) ∈ ℝ)
83	80, 82	lenltd 10062	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (((#‘𝑦) + 1) ≤ (#‘𝐵) ↔ ¬ (#‘𝐵) < ((#‘𝑦) + 1)))
84	68, 75, 83	3bitr3d 297	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝑦 ∪ {𝑧}) ≼ 𝐵 ↔ ¬ (#‘𝐵) < ((#‘𝑦) + 1)))
85	63, 84	sylibd 228	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → ¬ (#‘𝐵) < ((#‘𝑦) + 1)))
86	85	exlimdv 1848	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → ¬ (#‘𝐵) < ((#‘𝑦) + 1)))
87	61, 86	syl5bi 231	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ({𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} ≠ ∅ → ¬ (#‘𝐵) < ((#‘𝑦) + 1)))
88	87	necon4ad 2801	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘𝐵) < ((#‘𝑦) + 1) → {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} = ∅))
89	88	imp 444	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} = ∅)
90	89	fveq2d 6107	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = (#‘∅))
91		hashcl 13009	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∪ {𝑧}) ∈ Fin → (#‘(𝑦 ∪ {𝑧})) ∈ ℕ₀)
92	72, 91	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘(𝑦 ∪ {𝑧})) ∈ ℕ₀)
93		faccl 12932	. . . . . . . . . . . . 13 ⊢ ((#‘(𝑦 ∪ {𝑧})) ∈ ℕ₀ → (!‘(#‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
94	92, 93	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (!‘(#‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
95	94	nncnd 10913	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (!‘(#‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
96	95	adantr 480	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (!‘(#‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
97	96	mul01d 10114	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((!‘(#‘(𝑦 ∪ {𝑧}))) · 0) = 0)
98	19, 90, 97	3eqtr4a 2670	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · 0))
99	67	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))
100	99	oveq2d 6565	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))) = ((#‘𝐵)C((#‘𝑦) + 1)))
101	81	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘𝐵) ∈ ℕ₀)
102	79	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘𝑦) + 1) ∈ ℕ)
103	102	nnzd 11357	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘𝑦) + 1) ∈ ℤ)
104		simpr 476	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘𝐵) < ((#‘𝑦) + 1))
105	104	olcd 407	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (((#‘𝑦) + 1) < 0 ∨ (#‘𝐵) < ((#‘𝑦) + 1)))
106		bcval4 12956	. . . . . . . . . . 11 ⊢ (((#‘𝐵) ∈ ℕ₀ ∧ ((#‘𝑦) + 1) ∈ ℤ ∧ (((#‘𝑦) + 1) < 0 ∨ (#‘𝐵) < ((#‘𝑦) + 1))) → ((#‘𝐵)C((#‘𝑦) + 1)) = 0)
107	101, 103, 105, 106	syl3anc 1318	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘𝐵)C((#‘𝑦) + 1)) = 0)
108	100, 107	eqtrd 2644	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))) = 0)
109	108	oveq2d 6565	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · 0))
110	98, 109	eqtr4d 2647	. . . . . . 7 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))))
111	110	a1d 25	. . . . . 6 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))))))
112		oveq2 6557	. . . . . . 7 ⊢ ((#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) → (((#‘𝐵) − (#‘𝑦)) · (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})) = (((#‘𝐵) − (#‘𝑦)) · ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦)))))
113	69	adantr 480	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → 𝑦 ∈ Fin)
114	73	adantr 480	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → 𝐵 ∈ Fin)
115		simplrr 797	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ¬ 𝑧 ∈ 𝑦)
116		simpr 476	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝑦) + 1) ≤ (#‘𝐵))
117	113, 114, 115, 116	hashf1lem2 13097	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = (((#‘𝐵) − (#‘𝑦)) · (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})))
118	81	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝐵) ∈ ℕ₀)
119		faccl 12932	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐵) ∈ ℕ₀ → (!‘(#‘𝐵)) ∈ ℕ)
120	118, 119	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘𝐵)) ∈ ℕ)
121	120	nncnd 10913	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘𝐵)) ∈ ℂ)
122	77	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝑦) ∈ ℕ₀)
123		peano2nn0 11210	. . . . . . . . . . . . . . . 16 ⊢ ((#‘𝑦) ∈ ℕ₀ → ((#‘𝑦) + 1) ∈ ℕ₀)
124	122, 123	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝑦) + 1) ∈ ℕ₀)
125		nn0sub2 11315	. . . . . . . . . . . . . . 15 ⊢ ((((#‘𝑦) + 1) ∈ ℕ₀ ∧ (#‘𝐵) ∈ ℕ₀ ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − ((#‘𝑦) + 1)) ∈ ℕ₀)
126	124, 118, 116, 125	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − ((#‘𝑦) + 1)) ∈ ℕ₀)
127		faccl 12932	. . . . . . . . . . . . . 14 ⊢ (((#‘𝐵) − ((#‘𝑦) + 1)) ∈ ℕ₀ → (!‘((#‘𝐵) − ((#‘𝑦) + 1))) ∈ ℕ)
128	126, 127	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − ((#‘𝑦) + 1))) ∈ ℕ)
129	128	nncnd 10913	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − ((#‘𝑦) + 1))) ∈ ℂ)
130	128	nnne0d 10942	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − ((#‘𝑦) + 1))) ≠ 0)
131	121, 129, 130	divcld 10680	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) ∈ ℂ)
132		faccl 12932	. . . . . . . . . . . . 13 ⊢ (((#‘𝑦) + 1) ∈ ℕ₀ → (!‘((#‘𝑦) + 1)) ∈ ℕ)
133	124, 132	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝑦) + 1)) ∈ ℕ)
134	133	nncnd 10913	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝑦) + 1)) ∈ ℂ)
135	133	nnne0d 10942	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝑦) + 1)) ≠ 0)
136	131, 134, 135	divcan2d 10682	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘((#‘𝑦) + 1)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / (!‘((#‘𝑦) + 1)))) = ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))))
137	118	nn0cnd 11230	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝐵) ∈ ℂ)
138	122	nn0cnd 11230	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝑦) ∈ ℂ)
139	137, 138	subcld 10271	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − (#‘𝑦)) ∈ ℂ)
140		ax-1cn 9873	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
141		npcan 10169	. . . . . . . . . . . . . 14 ⊢ ((((#‘𝐵) − (#‘𝑦)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((#‘𝐵) − (#‘𝑦)) − 1) + 1) = ((#‘𝐵) − (#‘𝑦)))
142	139, 140, 141	sylancl 693	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((((#‘𝐵) − (#‘𝑦)) − 1) + 1) = ((#‘𝐵) − (#‘𝑦)))
143		1cnd 9935	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → 1 ∈ ℂ)
144	137, 138, 143	subsub4d 10302	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((#‘𝐵) − (#‘𝑦)) − 1) = ((#‘𝐵) − ((#‘𝑦) + 1)))
145	144, 126	eqeltrd 2688	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((#‘𝐵) − (#‘𝑦)) − 1) ∈ ℕ₀)
146		nn0p1nn 11209	. . . . . . . . . . . . . 14 ⊢ ((((#‘𝐵) − (#‘𝑦)) − 1) ∈ ℕ₀ → ((((#‘𝐵) − (#‘𝑦)) − 1) + 1) ∈ ℕ)
147	145, 146	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((((#‘𝐵) − (#‘𝑦)) − 1) + 1) ∈ ℕ)
148	142, 147	eqeltrrd 2689	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − (#‘𝑦)) ∈ ℕ)
149	148	nnne0d 10942	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − (#‘𝑦)) ≠ 0)
150	131, 139, 149	divcan2d 10682	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((#‘𝐵) − (#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦)))) = ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))))
151	136, 150	eqtr4d 2647	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘((#‘𝑦) + 1)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / (!‘((#‘𝑦) + 1)))) = (((#‘𝐵) − (#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦)))))
152	67	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))
153	152	fveq2d 6107	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘(𝑦 ∪ {𝑧}))) = (!‘((#‘𝑦) + 1)))
154		nn0uz 11598	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
155	124, 154	syl6eleq 2698	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝑦) + 1) ∈ (ℤ_≥‘0))
156	118	nn0zd 11356	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝐵) ∈ ℤ)
157		elfz5 12205	. . . . . . . . . . . . . 14 ⊢ ((((#‘𝑦) + 1) ∈ (ℤ_≥‘0) ∧ (#‘𝐵) ∈ ℤ) → (((#‘𝑦) + 1) ∈ (0...(#‘𝐵)) ↔ ((#‘𝑦) + 1) ≤ (#‘𝐵)))
158	155, 156, 157	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((#‘𝑦) + 1) ∈ (0...(#‘𝐵)) ↔ ((#‘𝑦) + 1) ≤ (#‘𝐵)))
159	116, 158	mpbird 246	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝑦) + 1) ∈ (0...(#‘𝐵)))
160		bcval2 12954	. . . . . . . . . . . 12 ⊢ (((#‘𝑦) + 1) ∈ (0...(#‘𝐵)) → ((#‘𝐵)C((#‘𝑦) + 1)) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · (!‘((#‘𝑦) + 1)))))
161	159, 160	syl 17	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵)C((#‘𝑦) + 1)) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · (!‘((#‘𝑦) + 1)))))
162	152	oveq2d 6565	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))) = ((#‘𝐵)C((#‘𝑦) + 1)))
163	121, 129, 134, 130, 135	divdiv1d 10711	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / (!‘((#‘𝑦) + 1))) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · (!‘((#‘𝑦) + 1)))))
164	161, 162, 163	3eqtr4d 2654	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))) = (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / (!‘((#‘𝑦) + 1))))
165	153, 164	oveq12d 6567	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))) = ((!‘((#‘𝑦) + 1)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / (!‘((#‘𝑦) + 1)))))
166	122, 154	syl6eleq 2698	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝑦) ∈ (ℤ_≥‘0))
167		peano2fzr 12225	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝑦) ∈ (ℤ_≥‘0) ∧ ((#‘𝑦) + 1) ∈ (0...(#‘𝐵))) → (#‘𝑦) ∈ (0...(#‘𝐵)))
168	166, 159, 167	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝑦) ∈ (0...(#‘𝐵)))
169		bcval2 12954	. . . . . . . . . . . . . 14 ⊢ ((#‘𝑦) ∈ (0...(#‘𝐵)) → ((#‘𝐵)C(#‘𝑦)) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − (#‘𝑦))) · (!‘(#‘𝑦)))))
170	168, 169	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵)C(#‘𝑦)) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − (#‘𝑦))) · (!‘(#‘𝑦)))))
171		elfzle2 12216	. . . . . . . . . . . . . . . . . 18 ⊢ ((#‘𝑦) ∈ (0...(#‘𝐵)) → (#‘𝑦) ≤ (#‘𝐵))
172	168, 171	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝑦) ≤ (#‘𝐵))
173		nn0sub2 11315	. . . . . . . . . . . . . . . . 17 ⊢ (((#‘𝑦) ∈ ℕ₀ ∧ (#‘𝐵) ∈ ℕ₀ ∧ (#‘𝑦) ≤ (#‘𝐵)) → ((#‘𝐵) − (#‘𝑦)) ∈ ℕ₀)
174	122, 118, 172, 173	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − (#‘𝑦)) ∈ ℕ₀)
175		faccl 12932	. . . . . . . . . . . . . . . 16 ⊢ (((#‘𝐵) − (#‘𝑦)) ∈ ℕ₀ → (!‘((#‘𝐵) − (#‘𝑦))) ∈ ℕ)
176	174, 175	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − (#‘𝑦))) ∈ ℕ)
177	176	nncnd 10913	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − (#‘𝑦))) ∈ ℂ)
178		faccl 12932	. . . . . . . . . . . . . . . 16 ⊢ ((#‘𝑦) ∈ ℕ₀ → (!‘(#‘𝑦)) ∈ ℕ)
179	122, 178	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘𝑦)) ∈ ℕ)
180	179	nncnd 10913	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘𝑦)) ∈ ℂ)
181	176	nnne0d 10942	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − (#‘𝑦))) ≠ 0)
182	179	nnne0d 10942	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘𝑦)) ≠ 0)
183	121, 177, 180, 181, 182	divdiv1d 10711	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) / (!‘(#‘𝑦))) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − (#‘𝑦))) · (!‘(#‘𝑦)))))
184	170, 183	eqtr4d 2647	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵)C(#‘𝑦)) = (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) / (!‘(#‘𝑦))))
185	184	oveq2d 6565	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) = ((!‘(#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) / (!‘(#‘𝑦)))))
186		facnn2 12931	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐵) − (#‘𝑦)) ∈ ℕ → (!‘((#‘𝐵) − (#‘𝑦))) = ((!‘(((#‘𝐵) − (#‘𝑦)) − 1)) · ((#‘𝐵) − (#‘𝑦))))
187	148, 186	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − (#‘𝑦))) = ((!‘(((#‘𝐵) − (#‘𝑦)) − 1)) · ((#‘𝐵) − (#‘𝑦))))
188	144	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(((#‘𝐵) − (#‘𝑦)) − 1)) = (!‘((#‘𝐵) − ((#‘𝑦) + 1))))
189	188	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(((#‘𝐵) − (#‘𝑦)) − 1)) · ((#‘𝐵) − (#‘𝑦))) = ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · ((#‘𝐵) − (#‘𝑦))))
190	187, 189	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − (#‘𝑦))) = ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · ((#‘𝐵) − (#‘𝑦))))
191	190	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · ((#‘𝐵) − (#‘𝑦)))))
192	121, 177, 181	divcld 10680	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) ∈ ℂ)
193	192, 180, 182	divcan2d 10682	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) / (!‘(#‘𝑦)))) = ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))))
194	121, 129, 139, 130, 149	divdiv1d 10711	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦))) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · ((#‘𝐵) − (#‘𝑦)))))
195	191, 193, 194	3eqtr4d 2654	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) / (!‘(#‘𝑦)))) = (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦))))
196	185, 195	eqtrd 2644	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) = (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦))))
197	196	oveq2d 6565	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((#‘𝐵) − (#‘𝑦)) · ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦)))) = (((#‘𝐵) − (#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦)))))
198	151, 165, 197	3eqtr4d 2654	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))) = (((#‘𝐵) − (#‘𝑦)) · ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦)))))
199	117, 198	eqeq12d 2625	. . . . . . 7 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))) ↔ (((#‘𝐵) − (#‘𝑦)) · (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})) = (((#‘𝐵) − (#‘𝑦)) · ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))))))
200	112, 199	syl5ibr 235	. . . . . 6 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))))))
201	111, 200, 82, 80	ltlecasei 10024	. . . . 5 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))))))
202	201	expcom 450	. . . 4 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝐵 ∈ Fin → ((#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))))))
203	202	a2d 29	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦)))) → (𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))))))
204	27, 36, 45, 54, 60, 203	findcard2s 8086	. 2 ⊢ (𝐴 ∈ Fin → (𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴)))))
205	204	imp 444	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 ≠ wne 2780 Vcvv 3173 ∪ cun 3538 ∅c0 3874 {csn 4125 class class class wbr 4583 Fn wfn 5799 –1-1→wf1 5801 ‘cfv 5804 (class class class)co 6549 ≼ cdom 7839 Fincfn 7841 ℂcc 9813 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 < clt 9953 ≤ cle 9954 − cmin 10145 / cdiv 10563 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 !cfa 12922 Ccbc 12951 #chash 12979

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-n0 11170 df-xnn0 11241 df-z 11255 df-uz 11564 df-fz 12198 df-seq 12664 df-fac 12923 df-bc 12952 df-hash 12980

This theorem is referenced by: hashfac 13099 birthdaylem2 24479

W3C validator