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 13445

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 6281	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:∅–1-1→𝐵))
2		f1fn 6286	. . . . . . . . . . . 12 ⊢ (𝑓:∅–1-1→𝐵 → 𝑓 Fn ∅)
3		fn0 6191	. . . . . . . . . . . 12 ⊢ (𝑓 Fn ∅ ↔ 𝑓 = ∅)
4	2, 3	sylib 209	. . . . . . . . . . 11 ⊢ (𝑓:∅–1-1→𝐵 → 𝑓 = ∅)
5		f10 6354	. . . . . . . . . . . 12 ⊢ ∅:∅–1-1→𝐵
6		f1eq1 6280	. . . . . . . . . . . 12 ⊢ (𝑓 = ∅ → (𝑓:∅–1-1→𝐵 ↔ ∅:∅–1-1→𝐵))
7	5, 6	mpbiri 249	. . . . . . . . . . 11 ⊢ (𝑓 = ∅ → 𝑓:∅–1-1→𝐵)
8	4, 7	impbii 200	. . . . . . . . . 10 ⊢ (𝑓:∅–1-1→𝐵 ↔ 𝑓 = ∅)
9		velsn 4352	. . . . . . . . . 10 ⊢ (𝑓 ∈ {∅} ↔ 𝑓 = ∅)
10	8, 9	bitr4i 269	. . . . . . . . 9 ⊢ (𝑓:∅–1-1→𝐵 ↔ 𝑓 ∈ {∅})
11	1, 10	syl6bb 278	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓 ∈ {∅}))
12	11	abbi1dv 2886	. . . . . . 7 ⊢ (𝑥 = ∅ → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {∅})
13	12	fveq2d 6381	. . . . . 6 ⊢ (𝑥 = ∅ → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (♯‘{∅}))
14		0ex 4952	. . . . . . 7 ⊢ ∅ ∈ V
15		hashsng 13364	. . . . . . 7 ⊢ (∅ ∈ V → (♯‘{∅}) = 1)
16	14, 15	ax-mp 5	. . . . . 6 ⊢ (♯‘{∅}) = 1
17	13, 16	syl6eq 2815	. . . . 5 ⊢ (𝑥 = ∅ → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = 1)
18		fveq2 6377	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
19		hash0 13363	. . . . . . . . 9 ⊢ (♯‘∅) = 0
20	18, 19	syl6eq 2815	. . . . . . . 8 ⊢ (𝑥 = ∅ → (♯‘𝑥) = 0)
21	20	fveq2d 6381	. . . . . . 7 ⊢ (𝑥 = ∅ → (!‘(♯‘𝑥)) = (!‘0))
22		fac0 13270	. . . . . . 7 ⊢ (!‘0) = 1
23	21, 22	syl6eq 2815	. . . . . 6 ⊢ (𝑥 = ∅ → (!‘(♯‘𝑥)) = 1)
24	20	oveq2d 6860	. . . . . 6 ⊢ (𝑥 = ∅ → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C0))
25	23, 24	oveq12d 6862	. . . . 5 ⊢ (𝑥 = ∅ → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = (1 · ((♯‘𝐵)C0)))
26	17, 25	eqeq12d 2780	. . . 4 ⊢ (𝑥 = ∅ → ((♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ 1 = (1 · ((♯‘𝐵)C0))))
27	26	imbi2d 331	. . 3 ⊢ (𝑥 = ∅ → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → 1 = (1 · ((♯‘𝐵)C0)))))
28		f1eq2 6281	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:𝑦–1-1→𝐵))
29	28	abbidv 2884	. . . . . 6 ⊢ (𝑥 = 𝑦 → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:𝑦–1-1→𝐵})
30	29	fveq2d 6381	. . . . 5 ⊢ (𝑥 = 𝑦 → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}))
31		2fveq3 6382	. . . . . 6 ⊢ (𝑥 = 𝑦 → (!‘(♯‘𝑥)) = (!‘(♯‘𝑦)))
32		fveq2 6377	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
33	32	oveq2d 6860	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝑦)))
34	31, 33	oveq12d 6862	. . . . 5 ⊢ (𝑥 = 𝑦 → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))
35	30, 34	eqeq12d 2780	. . . 4 ⊢ (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
36	35	imbi2d 331	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))))
37		f1eq2 6281	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵))
38	37	abbidv 2884	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵})
39	38	fveq2d 6381	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}))
40		2fveq3 6382	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (!‘(♯‘𝑥)) = (!‘(♯‘(𝑦 ∪ {𝑧}))))
41		fveq2 6377	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
42	41	oveq2d 6860	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))
43	40, 42	oveq12d 6862	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))
44	39, 43	eqeq12d 2780	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
45	44	imbi2d 331	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))))
46		f1eq2 6281	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑓:𝑥–1-1→𝐵 ↔ 𝑓:𝐴–1-1→𝐵))
47	46	abbidv 2884	. . . . . 6 ⊢ (𝑥 = 𝐴 → {𝑓 ∣ 𝑓:𝑥–1-1→𝐵} = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})
48	47	fveq2d 6381	. . . . 5 ⊢ (𝑥 = 𝐴 → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))
49		2fveq3 6382	. . . . . 6 ⊢ (𝑥 = 𝐴 → (!‘(♯‘𝑥)) = (!‘(♯‘𝐴)))
50		fveq2 6377	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴))
51	50	oveq2d 6860	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((♯‘𝐵)C(♯‘𝑥)) = ((♯‘𝐵)C(♯‘𝐴)))
52	49, 51	oveq12d 6862	. . . . 5 ⊢ (𝑥 = 𝐴 → ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))
53	48, 52	eqeq12d 2780	. . . 4 ⊢ (𝑥 = 𝐴 → ((♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥))) ↔ (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴)))))
54	53	imbi2d 331	. . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝑥–1-1→𝐵}) = ((!‘(♯‘𝑥)) · ((♯‘𝐵)C(♯‘𝑥)))) ↔ (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))))
55		hashcl 13352	. . . . . 6 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ₀)
56		bcn0 13304	. . . . . 6 ⊢ ((♯‘𝐵) ∈ ℕ₀ → ((♯‘𝐵)C0) = 1)
57	55, 56	syl 17	. . . . 5 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵)C0) = 1)
58	57	oveq2d 6860	. . . 4 ⊢ (𝐵 ∈ Fin → (1 · ((♯‘𝐵)C0)) = (1 · 1))
59		1t1e1 11442	. . . 4 ⊢ (1 · 1) = 1
60	58, 59	syl6req 2816	. . 3 ⊢ (𝐵 ∈ Fin → 1 = (1 · ((♯‘𝐵)C0)))
61		abn0 4121	. . . . . . . . . . . . 13 ⊢ ({𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} ≠ ∅ ↔ ∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵)
62		f1domg 8182	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
63	62	adantr 472	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → (𝑦 ∪ {𝑧}) ≼ 𝐵))
64		vex 3353	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑧 ∈ V
65		hashunsng 13386	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
67	66	adantl 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
68	67	breq1d 4821	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
69		simprl 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝑦 ∈ Fin)
70		snfi 8247	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ∈ Fin
71		unfi 8436	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
72	69, 70, 71	sylancl 580	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑦 ∪ {𝑧}) ∈ Fin)
73		simpl 474	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → 𝐵 ∈ Fin)
74		hashdom 13373	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
75	72, 73, 74	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘(𝑦 ∪ {𝑧})) ≤ (♯‘𝐵) ↔ (𝑦 ∪ {𝑧}) ≼ 𝐵))
76		hashcl 13352	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
77	76	ad2antrl 719	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝑦) ∈ ℕ₀)
78		nn0p1nn 11581	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑦) ∈ ℕ₀ → ((♯‘𝑦) + 1) ∈ ℕ)
79	77, 78	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝑦) + 1) ∈ ℕ)
80	79	nnred 11293	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝑦) + 1) ∈ ℝ)
81	55	adantr 472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝐵) ∈ ℕ₀)
82	81	nn0red 11601	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘𝐵) ∈ ℝ)
83	80, 82	lenltd 10439	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (((♯‘𝑦) + 1) ≤ (♯‘𝐵) ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
84	68, 75, 83	3bitr3d 300	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝑦 ∪ {𝑧}) ≼ 𝐵 ↔ ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
85	63, 84	sylibd 230	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
86	85	exlimdv 2028	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (∃𝑓 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵 → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
87	61, 86	syl5bi 233	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ({𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} ≠ ∅ → ¬ (♯‘𝐵) < ((♯‘𝑦) + 1)))
88	87	necon4ad 2956	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘𝐵) < ((♯‘𝑦) + 1) → {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} = ∅))
89	88	imp 395	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → {𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵} = ∅)
90	89	fveq2d 6381	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = (♯‘∅))
91		hashcl 13352	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∪ {𝑧}) ∈ Fin → (♯‘(𝑦 ∪ {𝑧})) ∈ ℕ₀)
92	72, 91	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (♯‘(𝑦 ∪ {𝑧})) ∈ ℕ₀)
93		faccl 13277	. . . . . . . . . . . . 13 ⊢ ((♯‘(𝑦 ∪ {𝑧})) ∈ ℕ₀ → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
94	92, 93	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℕ)
95	94	nncnd 11294	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
96	95	adantr 472	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) ∈ ℂ)
97	96	mul01d 10491	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0) = 0)
98	19, 90, 97	3eqtr4a 2825	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0))
99	67	adantr 472	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
100	99	oveq2d 6860	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1)))
101	81	adantr 472	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) ∈ ℕ₀)
102	79	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈ ℕ)
103	102	nnzd 11731	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝑦) + 1) ∈ ℤ)
104		simpr 477	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘𝐵) < ((♯‘𝑦) + 1))
105	104	olcd 900	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (((♯‘𝑦) + 1) < 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1)))
106		bcval4 13301	. . . . . . . . . . 11 ⊢ (((♯‘𝐵) ∈ ℕ₀ ∧ ((♯‘𝑦) + 1) ∈ ℤ ∧ (((♯‘𝑦) + 1) < 0 ∨ (♯‘𝐵) < ((♯‘𝑦) + 1))) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0)
107	101, 103, 105, 106	syl3anc 1490	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = 0)
108	100, 107	eqtrd 2799	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = 0)
109	108	oveq2d 6860	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · 0))
110	98, 109	eqtr4d 2802	. . . . . . 7 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))))
111	110	a1d 25	. . . . . 6 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ (♯‘𝐵) < ((♯‘𝑦) + 1)) → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
112		oveq2 6852	. . . . . . 7 ⊢ ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
113	69	adantr 472	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝑦 ∈ Fin)
114	73	adantr 472	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 𝐵 ∈ Fin)
115		simplrr 796	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ¬ 𝑧 ∈ 𝑦)
116		simpr 477	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ≤ (♯‘𝐵))
117	113, 114, 115, 116	hashf1lem2 13444	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})))
118	81	adantr 472	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ₀)
119		faccl 13277	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐵) ∈ ℕ₀ → (!‘(♯‘𝐵)) ∈ ℕ)
120	118, 119	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈ ℕ)
121	120	nncnd 11294	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝐵)) ∈ ℂ)
122	77	adantr 472	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℕ₀)
123		peano2nn0 11582	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑦) ∈ ℕ₀ → ((♯‘𝑦) + 1) ∈ ℕ₀)
124	122, 123	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ ℕ₀)
125		nn0sub2 11688	. . . . . . . . . . . . . . 15 ⊢ ((((♯‘𝑦) + 1) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ₀)
126	124, 118, 116, 125	syl3anc 1490	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ₀)
127		faccl 13277	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐵) − ((♯‘𝑦) + 1)) ∈ ℕ₀ → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℕ)
128	126, 127	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℕ)
129	128	nncnd 11294	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ∈ ℂ)
130	128	nnne0d 11324	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) ≠ 0)
131	121, 129, 130	divcld 11057	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) ∈ ℂ)
132		faccl 13277	. . . . . . . . . . . . 13 ⊢ (((♯‘𝑦) + 1) ∈ ℕ₀ → (!‘((♯‘𝑦) + 1)) ∈ ℕ)
133	124, 132	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈ ℕ)
134	133	nncnd 11294	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ∈ ℂ)
135	133	nnne0d 11324	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝑦) + 1)) ≠ 0)
136	131, 134, 135	divcan2d 11059	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))))
137	118	nn0cnd 11602	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ)
138	122	nn0cnd 11602	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ ℂ)
139	137, 138	subcld 10648	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ)
140		ax-1cn 10249	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
141		npcan 10546	. . . . . . . . . . . . . 14 ⊢ ((((♯‘𝐵) − (♯‘𝑦)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) = ((♯‘𝐵) − (♯‘𝑦)))
142	139, 140, 141	sylancl 580	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) = ((♯‘𝐵) − (♯‘𝑦)))
143		1cnd 10290	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → 1 ∈ ℂ)
144	137, 138, 143	subsub4d 10679	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) = ((♯‘𝐵) − ((♯‘𝑦) + 1)))
145	144, 126	eqeltrd 2844	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) − 1) ∈ ℕ₀)
146		nn0p1nn 11581	. . . . . . . . . . . . . 14 ⊢ ((((♯‘𝐵) − (♯‘𝑦)) − 1) ∈ ℕ₀ → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈ ℕ)
147	145, 146	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((((♯‘𝐵) − (♯‘𝑦)) − 1) + 1) ∈ ℕ)
148	142, 147	eqeltrrd 2845	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ)
149	148	nnne0d 11324	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ≠ 0)
150	131, 139, 149	divcan2d 11059	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))))
151	136, 150	eqtr4d 2802	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))))
152	67	adantr 472	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
153	152	fveq2d 6381	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘(𝑦 ∪ {𝑧}))) = (!‘((♯‘𝑦) + 1)))
154		nn0uz 11925	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
155	124, 154	syl6eleq 2854	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (ℤ_≥‘0))
156	118	nn0zd 11730	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
157		elfz5 12544	. . . . . . . . . . . . . 14 ⊢ ((((♯‘𝑦) + 1) ∈ (ℤ_≥‘0) ∧ (♯‘𝐵) ∈ ℤ) → (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
158	155, 156, 157	syl2anc 579	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) ↔ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)))
159	116, 158	mpbird 248	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)))
160		bcval2 13299	. . . . . . . . . . . 12 ⊢ (((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
161	159, 160	syl 17	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C((♯‘𝑦) + 1)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
162	152	oveq2d 6860	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = ((♯‘𝐵)C((♯‘𝑦) + 1)))
163	121, 129, 134, 130, 135	divdiv1d 11088	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · (!‘((♯‘𝑦) + 1)))))
164	161, 162, 163	3eqtr4d 2809	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1))))
165	153, 164	oveq12d 6862	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = ((!‘((♯‘𝑦) + 1)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / (!‘((♯‘𝑦) + 1)))))
166	122, 154	syl6eleq 2854	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (ℤ_≥‘0))
167		peano2fzr 12564	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝑦) ∈ (ℤ_≥‘0) ∧ ((♯‘𝑦) + 1) ∈ (0...(♯‘𝐵))) → (♯‘𝑦) ∈ (0...(♯‘𝐵)))
168	166, 159, 167	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ∈ (0...(♯‘𝐵)))
169		bcval2 13299	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑦) ∈ (0...(♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
170	168, 169	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
171		elfzle2 12555	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑦) ∈ (0...(♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵))
172	168, 171	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (♯‘𝑦) ≤ (♯‘𝐵))
173		nn0sub2 11688	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝑦) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝑦) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ₀)
174	122, 118, 172, 173	syl3anc 1490	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ₀)
175		faccl 13277	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ₀ → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℕ)
176	174, 175	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℕ)
177	176	nncnd 11294	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ∈ ℂ)
178		faccl 13277	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑦) ∈ ℕ₀ → (!‘(♯‘𝑦)) ∈ ℕ)
179	122, 178	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈ ℕ)
180	179	nncnd 11294	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ∈ ℂ)
181	176	nnne0d 11324	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) ≠ 0)
182	179	nnne0d 11324	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(♯‘𝑦)) ≠ 0)
183	121, 177, 180, 181, 182	divdiv1d 11088	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − (♯‘𝑦))) · (!‘(♯‘𝑦)))))
184	170, 183	eqtr4d 2802	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘𝐵)C(♯‘𝑦)) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦))))
185	184	oveq2d 6860	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) = ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))))
186		facnn2 13276	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐵) − (♯‘𝑦)) ∈ ℕ → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))))
187	148, 186	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))))
188	144	fveq2d 6381	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) = (!‘((♯‘𝐵) − ((♯‘𝑦) + 1))))
189	188	oveq1d 6859	. . . . . . . . . . . . . 14 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(((♯‘𝐵) − (♯‘𝑦)) − 1)) · ((♯‘𝐵) − (♯‘𝑦))) = ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))
190	187, 189	eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (!‘((♯‘𝐵) − (♯‘𝑦))) = ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦))))
191	190	oveq2d 6860	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))))
192	121, 177, 181	divcld 11057	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) ∈ ℂ)
193	192, 180, 182	divcan2d 11059	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))) = ((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))))
194	121, 129, 139, 130, 149	divdiv1d 11088	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))) = ((!‘(♯‘𝐵)) / ((!‘((♯‘𝐵) − ((♯‘𝑦) + 1))) · ((♯‘𝐵) − (♯‘𝑦)))))
195	191, 193, 194	3eqtr4d 2809	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − (♯‘𝑦)))) / (!‘(♯‘𝑦)))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))))
196	185, 195	eqtrd 2799	. . . . . . . . . 10 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) = (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦))))
197	196	oveq2d 6860	. . . . . . . . 9 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))) = (((♯‘𝐵) − (♯‘𝑦)) · (((!‘(♯‘𝐵)) / (!‘((♯‘𝐵) − ((♯‘𝑦) + 1)))) / ((♯‘𝐵) − (♯‘𝑦)))))
198	151, 165, 197	3eqtr4d 2809	. . . . . . . 8 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦)))))
199	117, 198	eqeq12d 2780	. . . . . . 7 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧})))) ↔ (((♯‘𝐵) − (♯‘𝑦)) · (♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵})) = (((♯‘𝐵) − (♯‘𝑦)) · ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))))))
200	112, 199	syl5ibr 237	. . . . . 6 ⊢ (((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) ∧ ((♯‘𝑦) + 1) ≤ (♯‘𝐵)) → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
201	111, 200, 82, 80	ltlecasei 10401	. . . . 5 ⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((♯‘{𝑓 ∣ 𝑓:𝑦–1-1→𝐵}) = ((!‘(♯‘𝑦)) · ((♯‘𝐵)C(♯‘𝑦))) → (♯‘{𝑓 ∣ 𝑓:(𝑦 ∪ {𝑧})–1-1→𝐵}) = ((!‘(♯‘(𝑦 ∪ {𝑧}))) · ((♯‘𝐵)C(♯‘(𝑦 ∪ {𝑧}))))))
202	201	expcom 402	. . . 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 8410	. 2 ⊢ (𝐴 ∈ Fin → (𝐵 ∈ Fin → (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴)))))
205	204	imp 395	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) = ((!‘(♯‘𝐴)) · ((♯‘𝐵)C(♯‘𝐴))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 ∨ wo 873 = wceq 1652 ∃wex 1874 ∈ wcel 2155 {cab 2751 ≠ wne 2937 Vcvv 3350 ∪ cun 3732 ∅c0 4081 {csn 4336 class class class wbr 4811 Fn wfn 6065 –1-1→wf1 6067 ‘cfv 6070 (class class class)co 6844 ≼ cdom 8160 Fincfn 8162 ℂcc 10189 0cc0 10191 1c1 10192 + caddc 10194 · cmul 10196 < clt 10330 ≤ cle 10331 − cmin 10522 / cdiv 10940 ℕcn 11276 ℕ₀cn0 11540 ℤcz 11626 ℤ_≥cuz 11889 ...cfz 12536 !cfa 13267 Ccbc 13296 ♯chash 13324

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-rep 4932 ax-sep 4943 ax-nul 4951 ax-pow 5003 ax-pr 5064 ax-un 7149 ax-cnex 10247 ax-resscn 10248 ax-1cn 10249 ax-icn 10250 ax-addcl 10251 ax-addrcl 10252 ax-mulcl 10253 ax-mulrcl 10254 ax-mulcom 10255 ax-addass 10256 ax-mulass 10257 ax-distr 10258 ax-i2m1 10259 ax-1ne0 10260 ax-1rid 10261 ax-rnegex 10262 ax-rrecex 10263 ax-cnre 10264 ax-pre-lttri 10265 ax-pre-lttrn 10266 ax-pre-ltadd 10267 ax-pre-mulgt0 10268

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-reu 3062 df-rmo 3063 df-rab 3064 df-v 3352 df-sbc 3599 df-csb 3694 df-dif 3737 df-un 3739 df-in 3741 df-ss 3748 df-pss 3750 df-nul 4082 df-if 4246 df-pw 4319 df-sn 4337 df-pr 4339 df-tp 4341 df-op 4343 df-uni 4597 df-int 4636 df-iun 4680 df-br 4812 df-opab 4874 df-mpt 4891 df-tr 4914 df-id 5187 df-eprel 5192 df-po 5200 df-so 5201 df-fr 5238 df-we 5240 df-xp 5285 df-rel 5286 df-cnv 5287 df-co 5288 df-dm 5289 df-rn 5290 df-res 5291 df-ima 5292 df-pred 5867 df-ord 5913 df-on 5914 df-lim 5915 df-suc 5916 df-iota 6033 df-fun 6072 df-fn 6073 df-f 6074 df-f1 6075 df-fo 6076 df-f1o 6077 df-fv 6078 df-riota 6805 df-ov 6847 df-oprab 6848 df-mpt2 6849 df-om 7266 df-1st 7368 df-2nd 7369 df-wrecs 7612 df-recs 7674 df-rdg 7712 df-1o 7766 df-2o 7767 df-oadd 7770 df-er 7949 df-map 8064 df-pm 8065 df-en 8163 df-dom 8164 df-sdom 8165 df-fin 8166 df-card 9018 df-cda 9245 df-pnf 10332 df-mnf 10333 df-xr 10334 df-ltxr 10335 df-le 10336 df-sub 10524 df-neg 10525 df-div 10941 df-nn 11277 df-n0 11541 df-xnn0 11613 df-z 11627 df-uz 11890 df-fz 12537 df-seq 13012 df-fac 13268 df-bc 13297 df-hash 13325

This theorem is referenced by: hashfac 13446 birthdaylem2 24973

W3C validator