Theorem ballotlemoex

Description: O is a set. (Contributed by Thierry Arnoux, 7-Dec-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	ballotlemoex	$$⊢O\in \mathrm{V}$$

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		ovex	$$⊢\left(1\dots M+N\right)\in \mathrm{V}$$
5	4	pwex	$$⊢𝒫\left(1\dots M+N\right)\in \mathrm{V}$$
6	3 5	rabex2	$$⊢O\in \mathrm{V}$$