Theorem ballotlemelo

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

	Ref	Expression
Hypotheses	ballotth.m	|- M e. NN
	ballotth.n	|- N e. NN
	ballotth.o	|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
Assertion	ballotlemelo	|- ( C e. O <-> ( C C_ ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) )

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	|- M e. NN
2		ballotth.n	|- N e. NN
3		ballotth.o	|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
4		fveqeq2	|- ( d = C -> ( ( # ` d ) = M <-> ( # ` C ) = M ) )
5		fveqeq2	|- ( c = d -> ( ( # ` c ) = M <-> ( # ` d ) = M ) )
6	5	cbvrabv	|- { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M } = { d e. ~P ( 1 ... ( M + N ) ) | ( # ` d ) = M }
7	3 6	eqtri	|- O = { d e. ~P ( 1 ... ( M + N ) ) | ( # ` d ) = M }
8	4 7	elrab2	|- ( C e. O <-> ( C e. ~P ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) )
9		ovex	|- ( 1 ... ( M + N ) ) e. _V
10	9	elpw2	|- ( C e. ~P ( 1 ... ( M + N ) ) <-> C C_ ( 1 ... ( M + N ) ) )
11	10	anbi1i	|- ( ( C e. ~P ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) <-> ( C C_ ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) )
12	8 11	bitri	|- ( C e. O <-> ( C C_ ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) )