Theorem ballotlemelo

Description: Elementhood in O . (Contributed by Thierry Arnoux, 17-Apr-2017)

	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	ballotlemelo	$$⊢C\in O\leftrightarrow \left(C\subseteq \left(1\dots M+N\right)\wedge \left|C\right|=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		fveqeq2	$$⊢d=C\to \left(\left|d\right|=M\leftrightarrow \left|C\right|=M\right)$$
5		fveqeq2	$$⊢c=d\to \left(\left|c\right|=M\leftrightarrow \left|d\right|=M\right)$$
6	5	cbvrabv	$$⊢\left\{c\in 𝒫\left(1\dots M+N\right)|\left|c\right|=M\right\}=\left\{d\in 𝒫\left(1\dots M+N\right)|\left|d\right|=M\right\}$$
7	3 6	eqtri	$$⊢O=\left\{d\in 𝒫\left(1\dots M+N\right)|\left|d\right|=M\right\}$$
8	4 7	elrab2	$$⊢C\in O\leftrightarrow \left(C\in 𝒫\left(1\dots M+N\right)\wedge \left|C\right|=M\right)$$
9		ovex	$$⊢\left(1\dots M+N\right)\in \mathrm{V}$$
10	9	elpw2	$$⊢C\in 𝒫\left(1\dots M+N\right)\leftrightarrow C\subseteq \left(1\dots M+N\right)$$
11	10	anbi1i	$$⊢\left(C\in 𝒫\left(1\dots M+N\right)\wedge \left|C\right|=M\right)\leftrightarrow \left(C\subseteq \left(1\dots M+N\right)\wedge \left|C\right|=M\right)$$
12	8 11	bitri	$$⊢C\in O\leftrightarrow \left(C\subseteq \left(1\dots M+N\right)\wedge \left|C\right|=M\right)$$