Theorem ballotlem1

Description: The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016)

	Ref	Expression
Hypotheses	ballotth.m	$$⊢M\in \mathbb{N}$$
	ballotth.n	$$⊢N\in \mathbb{N}$$
	ballotth.o	$$⊢O=\left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}$$
Assertion	ballotlem1	$$⊢\left|O\right|=\left(\genfrac{}{}{0ex}{}{M+N}{M}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	$$⊢M\in \mathbb{N}$$
2		ballotth.n	$$⊢N\in \mathbb{N}$$
3		ballotth.o	$$⊢O=\left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}$$
4	3	fveq2i	$$⊢\left|O\right|=\left|\left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}\right|$$
5		fzfi	$$⊢\left(1\dots M+N\right)\in \mathrm{Fin}$$
6	1	nnzi	$$⊢M\in \mathbb{Z}$$
7		hashbc	$$⊢\left(\left(1\dots M+N\right)\in \mathrm{Fin}\wedge M\in \mathbb{Z}\right)\to \left(\genfrac{}{}{0ex}{}{\left|\left(1\dots M+N\right)\right|}{M}\right)=\left|\left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}\right|$$
8	5 6 7	mp2an	$$⊢\left(\genfrac{}{}{0ex}{}{\left|\left(1\dots M+N\right)\right|}{M}\right)=\left|\left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}\right|$$
9	1 2	pm3.2i	$$⊢\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)$$
10		nnaddcl	$$⊢\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\to M+N\in \mathbb{N}$$
11		nnnn0	$$⊢M+N\in \mathbb{N}\to M+N\in {\mathbb{N}}_0$$
12	9 10 11	mp2b	$$⊢M+N\in {\mathbb{N}}_0$$
13		hashfz1	$$⊢M+N\in {\mathbb{N}}_0\to \left|\left(1\dots M+N\right)\right|=M+N$$
14	12 13	ax-mp	$$⊢\left|\left(1\dots M+N\right)\right|=M+N$$
15	14	oveq1i	$$⊢\left(\genfrac{}{}{0ex}{}{\left|\left(1\dots M+N\right)\right|}{M}\right)=\left(\genfrac{}{}{0ex}{}{M+N}{M}\right)$$
16	4 8 15	3eqtr2i	$$⊢\left|O\right|=\left(\genfrac{}{}{0ex}{}{M+N}{M}\right)$$