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	$⊢ (A \in Fin \land B \in Fin) \to \|\{f \| f : A \underset{1-1}{⟶} B\}\| = \|A\|! (\binom{\|B\|}{\|A\|})$

Proof

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

Metamath Proof Explorer

Theorem hashf1

Proof