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 13241

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 6097	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:∅–1-1→𝐵))
2		f1fn 6102	. . . . . . . . . . . 12 ⊢ (𝑓:∅–1-1→𝐵 → 𝑓 Fn ∅)
3		fn0 6011	. . . . . . . . . . . 12 ⊢ (𝑓 Fn ∅ ↔ 𝑓 = ∅)
4	2, 3	sylib 208	. . . . . . . . . . 11 ⊢ (𝑓:∅–1-1→𝐵 → 𝑓 = ∅)
5		f10 6169	. . . . . . . . . . . 12 ⊢ ∅:∅–1-1→𝐵
6		f1eq1 6096	. . . . . . . . . . . 12 ⊢ (𝑓 = ∅ → (𝑓:∅–1-1→𝐵 ↔ ∅:∅–1-1→𝐵))
7	5, 6	mpbiri 248	. . . . . . . . . . 11 ⊢ (𝑓 = ∅ → 𝑓:∅–1-1→𝐵)
8	4, 7	impbii 199	. . . . . . . . . 10 ⊢ (𝑓:∅–1-1→𝐵 ↔ 𝑓 = ∅)
9		velsn 4193	. . . . . . . . . 10 ⊢ (𝑓 ∈ {∅} ↔ 𝑓 = ∅)
10	8, 9	bitr4i 267	. . . . . . . . 9 ⊢ (𝑓:∅–1-1→𝐵 ↔ 𝑓 ∈ {∅})
11	1, 10	syl6bb 276	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓 ∈ {∅}))
12	11	abbi1dv 2743	. . . . . . 7 ⊢ (𝑥 = ∅ → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {∅})
13	12	fveq2d 6195	. . . . . 6 ⊢ (𝑥 = ∅ → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (#‘{∅}))
14		0ex 4790	. . . . . . 7 ⊢ ∅ ∈ V
15		hashsng 13159	. . . . . . 7 ⊢ (∅ ∈ V → (#‘{∅}) = 1)
16	14, 15	ax-mp 5	. . . . . 6 ⊢ (#‘{∅}) = 1
17	13, 16	syl6eq 2672	. . . . 5 ⊢ (𝑥 = ∅ → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = 1)
18		fveq2 6191	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (#‘𝑥) = (#‘∅))
19		hash0 13158	. . . . . . . . 9 ⊢ (#‘∅) = 0
20	18, 19	syl6eq 2672	. . . . . . . 8 ⊢ (𝑥 = ∅ → (#‘𝑥) = 0)
21	20	fveq2d 6195	. . . . . . 7 ⊢ (𝑥 = ∅ → (!‘(#‘𝑥)) = (!‘0))
22		fac0 13063	. . . . . . 7 ⊢ (!‘0) = 1
23	21, 22	syl6eq 2672	. . . . . 6 ⊢ (𝑥 = ∅ → (!‘(#‘𝑥)) = 1)
24	20	oveq2d 6666	. . . . . 6 ⊢ (𝑥 = ∅ → ((#‘𝐵)C(#‘𝑥)) = ((#‘𝐵)C0))
25	23, 24	oveq12d 6668	. . . . 5 ⊢ (𝑥 = ∅ → ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) = (1 · ((#‘𝐵)C0)))
26	17, 25	eqeq12d 2637	. . . 4 ⊢ (𝑥 = ∅ → ((#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) ↔ 1 = (1 · ((#‘𝐵)C0))))
27	26	imbi2d 330	. . 3 ⊢ (𝑥 = ∅ → ((𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥)))) ↔ (𝐵 ∈ Fin → 1 = (1 · ((#‘𝐵)C0)))))
28		f1eq2 6097	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:𝑦–1-1→𝐵))
29	28	abbidv 2741	. . . . . 6 ⊢ (𝑥 = 𝑦 → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:𝑦–1-1→𝐵})
30	29	fveq2d 6195	. . . . 5 ⊢ (𝑥 = 𝑦 → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}))
31		fveq2 6191	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦))
32	31	fveq2d 6195	. . . . . 6 ⊢ (𝑥 = 𝑦 → (!‘(#‘𝑥)) = (!‘(#‘𝑦)))
33	31	oveq2d 6666	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((#‘𝐵)C(#‘𝑥)) = ((#‘𝐵)C(#‘𝑦)))
34	32, 33	oveq12d 6668	. . . . 5 ⊢ (𝑥 = 𝑦 → ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))))
35	30, 34	eqeq12d 2637	. . . 4 ⊢ (𝑥 = 𝑦 → ((#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) ↔ (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦)))))
36	35	imbi2d 330	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥)))) ↔ (𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))))))
37		f1eq2 6097	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵))
38	37	abbidv 2741	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵})
39	38	fveq2d 6195	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}))
40		fveq2 6191	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑦 ∪ {𝑧})))
41	40	fveq2d 6195	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (!‘(#‘𝑥)) = (!‘(#‘(𝑦 ∪ {𝑧}))))
42	40	oveq2d 6666	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘𝐵)C(#‘𝑥)) = ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))))
43	41, 42	oveq12d 6668	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))))
44	39, 43	eqeq12d 2637	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) ↔ (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))))))
45	44	imbi2d 330	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥)))) ↔ (𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))))))
46		f1eq2 6097	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:𝐴–1-1→𝐵))
47	46	abbidv 2741	. . . . . 6 ⊢ (𝑥 = 𝐴 → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})
48	47	fveq2d 6195	. . . . 5 ⊢ (𝑥 = 𝐴 → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))
49		fveq2 6191	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (#‘𝑥) = (#‘𝐴))
50	49	fveq2d 6195	. . . . . 6 ⊢ (𝑥 = 𝐴 → (!‘(#‘𝑥)) = (!‘(#‘𝐴)))
51	49	oveq2d 6666	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((#‘𝐵)C(#‘𝑥)) = ((#‘𝐵)C(#‘𝐴)))
52	50, 51	oveq12d 6668	. . . . 5 ⊢ (𝑥 = 𝐴 → ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴))))
53	48, 52	eqeq12d 2637	. . . 4 ⊢ (𝑥 = 𝐴 → ((#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥))) ↔ (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴)))))
54	53	imbi2d 330	. . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(#‘𝑥)) · ((#‘𝐵)C(#‘𝑥)))) ↔ (𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴))))))
55		hashcl 13147	. . . . . 6 ⊢ (𝐵 ∈ Fin → (#‘𝐵) ∈ ℕ₀)
56		bcn0 13097	. . . . . 6 ⊢ ((#‘𝐵) ∈ ℕ₀ → ((#‘𝐵)C0) = 1)
57	55, 56	syl 17	. . . . 5 ⊢ (𝐵 ∈ Fin → ((#‘𝐵)C0) = 1)
58	57	oveq2d 6666	. . . 4 ⊢ (𝐵 ∈ Fin → (1 · ((#‘𝐵)C0)) = (1 · 1))
59		1t1e1 11175	. . . 4 ⊢ (1 · 1) = 1
60	58, 59	syl6req 2673	. . 3 ⊢ (𝐵 ∈ Fin → 1 = (1 · ((#‘𝐵)C0)))
61		abn0 3954	. . . . . . . . . . . . 13 ⊢ ({𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} ≠ ∅ ↔ ∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵)
62		f1domg 7975	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
63	62	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
64		vex 3203	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑧 ∈ V
65		hashunsng 13181	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1)))
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))
67	66	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))
68	67	breq1d 4663	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘(𝑦 ∪ {𝑧})) ≤ (#‘𝐵) ↔ ((#‘𝑦) + 1) ≤ (#‘𝐵)))
69		simprl 794	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin)
70		snfi 8038	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ∈ Fin
71		unfi 8227	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
72	69, 70, 71	sylancl 694	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin)
73		simpl 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐵 ∈ Fin)
74		hashdom 13168	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘(𝑦 ∪ {𝑧})) ≤ (#‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
75	72, 73, 74	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘(𝑦 ∪ {𝑧})) ≤ (#‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
76		hashcl 13147	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ Fin → (#‘𝑦) ∈ ℕ₀)
77	76	ad2antrl 764	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘𝑦) ∈ ℕ₀)
78		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . 19 ⊢ ((#‘𝑦) ∈ ℕ₀ → ((#‘𝑦) + 1) ∈ ℕ)
79	77, 78	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘𝑦) + 1) ∈ ℕ)
80	79	nnred 11035	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘𝑦) + 1) ∈ ℝ)
81	55	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘𝐵) ∈ ℕ₀)
82	81	nn0red 11352	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘𝐵) ∈ ℝ)
83	80, 82	lenltd 10183	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (((#‘𝑦) + 1) ≤ (#‘𝐵) ↔ ¬ (#‘𝐵) < ((#‘𝑦) + 1)))
84	68, 75, 83	3bitr3d 298	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝑦 ∪ {𝑧}) ≼ 𝐵 ↔ ¬ (#‘𝐵) < ((#‘𝑦) + 1)))
85	63, 84	sylibd 229	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → ¬ (#‘𝐵) < ((#‘𝑦) + 1)))
86	85	exlimdv 1861	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → ¬ (#‘𝐵) < ((#‘𝑦) + 1)))
87	61, 86	syl5bi 232	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ({𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} ≠ ∅ → ¬ (#‘𝐵) < ((#‘𝑦) + 1)))
88	87	necon4ad 2813	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘𝐵) < ((#‘𝑦) + 1) → {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} = ∅))
89	88	imp 445	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} = ∅)
90	89	fveq2d 6195	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = (#‘∅))
91		hashcl 13147	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∪ {𝑧}) ∈ Fin → (#‘(𝑦 ∪ {𝑧})) ∈ ℕ₀)
92	72, 91	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (#‘(𝑦 ∪ {𝑧})) ∈ ℕ₀)
93		faccl 13070	. . . . . . . . . . . . 13 ⊢ ((#‘(𝑦 ∪ {𝑧})) ∈ ℕ₀ → (!‘(#‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
94	92, 93	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (!‘(#‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
95	94	nncnd 11036	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (!‘(#‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
96	95	adantr 481	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (!‘(#‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
97	96	mul01d 10235	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((!‘(#‘(𝑦 ∪ {𝑧}))) · 0) = 0)
98	19, 90, 97	3eqtr4a 2682	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · 0))
99	67	adantr 481	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))
100	99	oveq2d 6666	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))) = ((#‘𝐵)C((#‘𝑦) + 1)))
101	81	adantr 481	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘𝐵) ∈ ℕ₀)
102	79	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘𝑦) + 1) ∈ ℕ)
103	102	nnzd 11481	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘𝑦) + 1) ∈ ℤ)
104		simpr 477	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘𝐵) < ((#‘𝑦) + 1))
105	104	olcd 408	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (((#‘𝑦) + 1) < 0 ∨ (#‘𝐵) < ((#‘𝑦) + 1)))
106		bcval4 13094	. . . . . . . . . . 11 ⊢ (((#‘𝐵) ∈ ℕ₀ ∧ ((#‘𝑦) + 1) ∈ ℤ ∧ (((#‘𝑦) + 1) < 0 ∨ (#‘𝐵) < ((#‘𝑦) + 1))) → ((#‘𝐵)C((#‘𝑦) + 1)) = 0)
107	101, 103, 105, 106	syl3anc 1326	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘𝐵)C((#‘𝑦) + 1)) = 0)
108	100, 107	eqtrd 2656	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))) = 0)
109	108	oveq2d 6666	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · 0))
110	98, 109	eqtr4d 2659	. . . . . . 7 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))))
111	110	a1d 25	. . . . . 6 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (#‘𝐵) < ((#‘𝑦) + 1)) → ((#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))))))
112		oveq2 6658	. . . . . . 7 ⊢ ((#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) → (((#‘𝐵) − (#‘𝑦)) · (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})) = (((#‘𝐵) − (#‘𝑦)) · ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦)))))
113	69	adantr 481	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → 𝑦 ∈ Fin)
114	73	adantr 481	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → 𝐵 ∈ Fin)
115		simplrr 801	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ¬ 𝑧 ∈ 𝑦)
116		simpr 477	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝑦) + 1) ≤ (#‘𝐵))
117	113, 114, 115, 116	hashf1lem2 13240	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = (((#‘𝐵) − (#‘𝑦)) · (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})))
118	81	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝐵) ∈ ℕ₀)
119		faccl 13070	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐵) ∈ ℕ₀ → (!‘(#‘𝐵)) ∈ ℕ)
120	118, 119	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘𝐵)) ∈ ℕ)
121	120	nncnd 11036	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘𝐵)) ∈ ℂ)
122	77	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝑦) ∈ ℕ₀)
123		peano2nn0 11333	. . . . . . . . . . . . . . . 16 ⊢ ((#‘𝑦) ∈ ℕ₀ → ((#‘𝑦) + 1) ∈ ℕ₀)
124	122, 123	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝑦) + 1) ∈ ℕ₀)
125		nn0sub2 11438	. . . . . . . . . . . . . . 15 ⊢ ((((#‘𝑦) + 1) ∈ ℕ₀ ∧ (#‘𝐵) ∈ ℕ₀ ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − ((#‘𝑦) + 1)) ∈ ℕ₀)
126	124, 118, 116, 125	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − ((#‘𝑦) + 1)) ∈ ℕ₀)
127		faccl 13070	. . . . . . . . . . . . . 14 ⊢ (((#‘𝐵) − ((#‘𝑦) + 1)) ∈ ℕ₀ → (!‘((#‘𝐵) − ((#‘𝑦) + 1))) ∈ ℕ)
128	126, 127	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − ((#‘𝑦) + 1))) ∈ ℕ)
129	128	nncnd 11036	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − ((#‘𝑦) + 1))) ∈ ℂ)
130	128	nnne0d 11065	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − ((#‘𝑦) + 1))) ≠ 0)
131	121, 129, 130	divcld 10801	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) ∈ ℂ)
132		faccl 13070	. . . . . . . . . . . . 13 ⊢ (((#‘𝑦) + 1) ∈ ℕ₀ → (!‘((#‘𝑦) + 1)) ∈ ℕ)
133	124, 132	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝑦) + 1)) ∈ ℕ)
134	133	nncnd 11036	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝑦) + 1)) ∈ ℂ)
135	133	nnne0d 11065	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝑦) + 1)) ≠ 0)
136	131, 134, 135	divcan2d 10803	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘((#‘𝑦) + 1)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / (!‘((#‘𝑦) + 1)))) = ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))))
137	118	nn0cnd 11353	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝐵) ∈ ℂ)
138	122	nn0cnd 11353	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝑦) ∈ ℂ)
139	137, 138	subcld 10392	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − (#‘𝑦)) ∈ ℂ)
140		ax-1cn 9994	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
141		npcan 10290	. . . . . . . . . . . . . 14 ⊢ ((((#‘𝐵) − (#‘𝑦)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((#‘𝐵) − (#‘𝑦)) − 1) + 1) = ((#‘𝐵) − (#‘𝑦)))
142	139, 140, 141	sylancl 694	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((((#‘𝐵) − (#‘𝑦)) − 1) + 1) = ((#‘𝐵) − (#‘𝑦)))
143		1cnd 10056	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → 1 ∈ ℂ)
144	137, 138, 143	subsub4d 10423	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((#‘𝐵) − (#‘𝑦)) − 1) = ((#‘𝐵) − ((#‘𝑦) + 1)))
145	144, 126	eqeltrd 2701	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((#‘𝐵) − (#‘𝑦)) − 1) ∈ ℕ₀)
146		nn0p1nn 11332	. . . . . . . . . . . . . 14 ⊢ ((((#‘𝐵) − (#‘𝑦)) − 1) ∈ ℕ₀ → ((((#‘𝐵) − (#‘𝑦)) − 1) + 1) ∈ ℕ)
147	145, 146	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((((#‘𝐵) − (#‘𝑦)) − 1) + 1) ∈ ℕ)
148	142, 147	eqeltrrd 2702	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − (#‘𝑦)) ∈ ℕ)
149	148	nnne0d 11065	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − (#‘𝑦)) ≠ 0)
150	131, 139, 149	divcan2d 10803	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((#‘𝐵) − (#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦)))) = ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))))
151	136, 150	eqtr4d 2659	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘((#‘𝑦) + 1)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / (!‘((#‘𝑦) + 1)))) = (((#‘𝐵) − (#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦)))))
152	67	adantr 481	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))
153	152	fveq2d 6195	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘(𝑦 ∪ {𝑧}))) = (!‘((#‘𝑦) + 1)))
154		nn0uz 11722	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
155	124, 154	syl6eleq 2711	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝑦) + 1) ∈ (ℤ_≥‘0))
156	118	nn0zd 11480	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝐵) ∈ ℤ)
157		elfz5 12334	. . . . . . . . . . . . . 14 ⊢ ((((#‘𝑦) + 1) ∈ (ℤ_≥‘0) ∧ (#‘𝐵) ∈ ℤ) → (((#‘𝑦) + 1) ∈ (0...(#‘𝐵)) ↔ ((#‘𝑦) + 1) ≤ (#‘𝐵)))
158	155, 156, 157	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((#‘𝑦) + 1) ∈ (0...(#‘𝐵)) ↔ ((#‘𝑦) + 1) ≤ (#‘𝐵)))
159	116, 158	mpbird 247	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝑦) + 1) ∈ (0...(#‘𝐵)))
160		bcval2 13092	. . . . . . . . . . . 12 ⊢ (((#‘𝑦) + 1) ∈ (0...(#‘𝐵)) → ((#‘𝐵)C((#‘𝑦) + 1)) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · (!‘((#‘𝑦) + 1)))))
161	159, 160	syl 17	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵)C((#‘𝑦) + 1)) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · (!‘((#‘𝑦) + 1)))))
162	152	oveq2d 6666	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))) = ((#‘𝐵)C((#‘𝑦) + 1)))
163	121, 129, 134, 130, 135	divdiv1d 10832	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / (!‘((#‘𝑦) + 1))) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · (!‘((#‘𝑦) + 1)))))
164	161, 162, 163	3eqtr4d 2666	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))) = (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / (!‘((#‘𝑦) + 1))))
165	153, 164	oveq12d 6668	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))) = ((!‘((#‘𝑦) + 1)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / (!‘((#‘𝑦) + 1)))))
166	122, 154	syl6eleq 2711	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝑦) ∈ (ℤ_≥‘0))
167		peano2fzr 12354	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝑦) ∈ (ℤ_≥‘0) ∧ ((#‘𝑦) + 1) ∈ (0...(#‘𝐵))) → (#‘𝑦) ∈ (0...(#‘𝐵)))
168	166, 159, 167	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝑦) ∈ (0...(#‘𝐵)))
169		bcval2 13092	. . . . . . . . . . . . . 14 ⊢ ((#‘𝑦) ∈ (0...(#‘𝐵)) → ((#‘𝐵)C(#‘𝑦)) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − (#‘𝑦))) · (!‘(#‘𝑦)))))
170	168, 169	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵)C(#‘𝑦)) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − (#‘𝑦))) · (!‘(#‘𝑦)))))
171		elfzle2 12345	. . . . . . . . . . . . . . . . . 18 ⊢ ((#‘𝑦) ∈ (0...(#‘𝐵)) → (#‘𝑦) ≤ (#‘𝐵))
172	168, 171	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (#‘𝑦) ≤ (#‘𝐵))
173		nn0sub2 11438	. . . . . . . . . . . . . . . . 17 ⊢ (((#‘𝑦) ∈ ℕ₀ ∧ (#‘𝐵) ∈ ℕ₀ ∧ (#‘𝑦) ≤ (#‘𝐵)) → ((#‘𝐵) − (#‘𝑦)) ∈ ℕ₀)
174	122, 118, 172, 173	syl3anc 1326	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵) − (#‘𝑦)) ∈ ℕ₀)
175		faccl 13070	. . . . . . . . . . . . . . . 16 ⊢ (((#‘𝐵) − (#‘𝑦)) ∈ ℕ₀ → (!‘((#‘𝐵) − (#‘𝑦))) ∈ ℕ)
176	174, 175	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − (#‘𝑦))) ∈ ℕ)
177	176	nncnd 11036	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − (#‘𝑦))) ∈ ℂ)
178		faccl 13070	. . . . . . . . . . . . . . . 16 ⊢ ((#‘𝑦) ∈ ℕ₀ → (!‘(#‘𝑦)) ∈ ℕ)
179	122, 178	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘𝑦)) ∈ ℕ)
180	179	nncnd 11036	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘𝑦)) ∈ ℂ)
181	176	nnne0d 11065	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − (#‘𝑦))) ≠ 0)
182	179	nnne0d 11065	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(#‘𝑦)) ≠ 0)
183	121, 177, 180, 181, 182	divdiv1d 10832	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) / (!‘(#‘𝑦))) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − (#‘𝑦))) · (!‘(#‘𝑦)))))
184	170, 183	eqtr4d 2659	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘𝐵)C(#‘𝑦)) = (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) / (!‘(#‘𝑦))))
185	184	oveq2d 6666	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) = ((!‘(#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) / (!‘(#‘𝑦)))))
186		facnn2 13069	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐵) − (#‘𝑦)) ∈ ℕ → (!‘((#‘𝐵) − (#‘𝑦))) = ((!‘(((#‘𝐵) − (#‘𝑦)) − 1)) · ((#‘𝐵) − (#‘𝑦))))
187	148, 186	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − (#‘𝑦))) = ((!‘(((#‘𝐵) − (#‘𝑦)) − 1)) · ((#‘𝐵) − (#‘𝑦))))
188	144	fveq2d 6195	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘(((#‘𝐵) − (#‘𝑦)) − 1)) = (!‘((#‘𝐵) − ((#‘𝑦) + 1))))
189	188	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(((#‘𝐵) − (#‘𝑦)) − 1)) · ((#‘𝐵) − (#‘𝑦))) = ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · ((#‘𝐵) − (#‘𝑦))))
190	187, 189	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (!‘((#‘𝐵) − (#‘𝑦))) = ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · ((#‘𝐵) − (#‘𝑦))))
191	190	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · ((#‘𝐵) − (#‘𝑦)))))
192	121, 177, 181	divcld 10801	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) ∈ ℂ)
193	192, 180, 182	divcan2d 10803	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) / (!‘(#‘𝑦)))) = ((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))))
194	121, 129, 139, 130, 149	divdiv1d 10832	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦))) = ((!‘(#‘𝐵)) / ((!‘((#‘𝐵) − ((#‘𝑦) + 1))) · ((#‘𝐵) − (#‘𝑦)))))
195	191, 193, 194	3eqtr4d 2666	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − (#‘𝑦)))) / (!‘(#‘𝑦)))) = (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦))))
196	185, 195	eqtrd 2656	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) = (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦))))
197	196	oveq2d 6666	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → (((#‘𝐵) − (#‘𝑦)) · ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦)))) = (((#‘𝐵) − (#‘𝑦)) · (((!‘(#‘𝐵)) / (!‘((#‘𝐵) − ((#‘𝑦) + 1)))) / ((#‘𝐵) − (#‘𝑦)))))
198	151, 165, 197	3eqtr4d 2666	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))) = (((#‘𝐵) − (#‘𝑦)) · ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦)))))
199	117, 198	eqeq12d 2637	. . . . . . 7 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧})))) ↔ (((#‘𝐵) − (#‘𝑦)) · (#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})) = (((#‘𝐵) − (#‘𝑦)) · ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))))))
200	112, 199	syl5ibr 236	. . . . . 6 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((#‘𝑦) + 1) ≤ (#‘𝐵)) → ((#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))))))
201	111, 200, 82, 80	ltlecasei 10145	. . . . 5 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((#‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(#‘𝑦)) · ((#‘𝐵)C(#‘𝑦))) → (#‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(#‘(𝑦 ∪ {𝑧}))) · ((#‘𝐵)C(#‘(𝑦 ∪ {𝑧}))))))
202	201	expcom 451	. . . 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 8201	. 2 ⊢ (𝐴 ∈ Fin → (𝐵 ∈ Fin → (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴)))))
205	204	imp 445	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(#‘𝐴)) · ((#‘𝐵)C(#‘𝐴))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 = wceq 1483 ∃wex 1704 ∈ wcel 1990 {cab 2608 ≠ wne 2794 Vcvv 3200 ∪ cun 3572 ∅c0 3915 {csn 4177 class class class wbr 4653 Fn wfn 5883 –1-1→wf1 5885 ‘cfv 5888 (class class class)co 6650 ≼ cdom 7953 Fincfn 7955 ℂcc 9934 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ...cfz 12326 !cfa 13060 Ccbc 13089 #chash 13117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-seq 12802 df-fac 13061 df-bc 13090 df-hash 13118

This theorem is referenced by: hashfac 13242 birthdaylem2 24679

W3C validator