Theorem ballotlemelo 24698

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

Hypotheses

Ref	Expression
ballotth.m	|- M e. NN
ballotth.n	|- N e. NN
ballotth.o	|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }

Assertion

Ref	Expression
ballotlemelo	|- ( C e. O <-> ( C C_ ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) )

Distinct variable groups:   M, c   N, c   O, c

Allowed substitution hint:   C( c)

Proof of Theorem ballotlemelo

Dummy variable d is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5687	. . . 4 |- ( d = C -> ( # ` d ) = ( # ` C ) )
2	1	eqeq1d 2412	. . 3 |- ( d = C -> ( ( # ` d ) = M <-> ( # ` C ) = M ) )
3		ballotth.o	. . . 4 |- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
4		fveq2 5687	. . . . . 6 |- ( c = d -> ( # ` c ) = ( # ` d ) )
5	4	eqeq1d 2412	. . . . 5 |- ( c = d -> ( ( # ` c ) = M <-> ( # ` d ) = M ) )
6	5	cbvrabv 2915	. . . 4 |- { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M } = { d e. ~P ( 1 ... ( M + N ) ) | ( # ` d ) = M }
7	3, 6	eqtri 2424	. . 3 |- O = { d e. ~P ( 1 ... ( M + N ) ) | ( # ` d ) = M }
8	2, 7	elrab2 3054	. 2 |- ( C e. O <-> ( C e. ~P ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) )
9		ovex 6065	. . . 4 |- ( 1 ... ( M + N ) ) e. _V
10	9	elpw2 4324	. . 3 |- ( C e. ~P ( 1 ... ( M + N ) ) <-> C C_ ( 1 ... ( M + N ) ) )
11	10	anbi1i 677	. 2 |- ( ( C e. ~P ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) <-> ( C C_ ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) )
12	8, 11	bitri 241	1 |- ( C e. O <-> ( C C_ ( 1 ... ( M + N ) ) /\ ( # ` C ) = M ) )

Syntax hints:   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   {crab 2670   C_ wss 3280   ~Pcpw 3759   ` cfv 5413  (class class class)co 6040   1c1 8947   + caddc 8949   NNcn 9956   ...cfz 10999   #chash 11573

This theorem is referenced by:  ballotlemscr  24729  ballotlemro  24733  ballotlemfg  24736  ballotlemfrc  24737  ballotlemfrceq  24739  ballotlemrinv0  24743

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043