hashbc2

Description: The size of the binomial set is the binomial coefficient. (Contributed by Mario Carneiro, 20-Apr-2015)

		Ref	Expression
	Hypothesis	ramval.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
	Assertion	hashbc2	$⊢ (A \in Fin \land N \in ℕ_{0}) \to \|A C N\| = (\binom{\|A\|}{N})$

Step	Hyp	Ref	Expression
1		ramval.c	$⊢ C = (a \in V, i \in ℕ_{0} ⟼ \{b \in 𝒫 a \| \|b\| = i\})$
2	1	hashbcval	$⊢ (A \in Fin \land N \in ℕ_{0}) \to A C N = \{x \in 𝒫 A \| \|x\| = N\}$
3	2	fveq2d	$⊢ (A \in Fin \land N \in ℕ_{0}) \to \|A C N\| = \|\{x \in 𝒫 A \| \|x\| = N\}\|$
4		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
5		hashbc	$⊢ (A \in Fin \land N \in ℤ) \to (\binom{\|A\|}{N}) = \|\{x \in 𝒫 A \| \|x\| = N\}\|$
6	4 5	sylan2	$⊢ (A \in Fin \land N \in ℕ_{0}) \to (\binom{\|A\|}{N}) = \|\{x \in 𝒫 A \| \|x\| = N\}\|$
7	3 6	eqtr4d	$⊢ (A \in Fin \land N \in ℕ_{0}) \to \|A C N\| = (\binom{\|A\|}{N})$

Metamath Proof Explorer