Metamath Proof Explorer

Theorem ballotleme

Description: Elements of E . (Contributed by Thierry Arnoux, 14-Dec-2016)

Ref Expression
Hypotheses ballotth.m ⊢M∈ℕ
ballotth.n ⊢N∈ℕ
ballotth.o ⊢O=c∈𝒫1…M+N|c=M
ballotth.p ⊢P=x∈𝒫O⟼xO
ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
Assertion ballotleme ⊢C∈E↔C∈O∧∀i∈1…M+N0<F⁡C⁡i

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢M∈ℕ
2 ballotth.n ⊢N∈ℕ
3 ballotth.o ⊢O=c∈𝒫1…M+N|c=M
4 ballotth.p ⊢P=x∈𝒫O⟼xO
5 ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
6 ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
7 fveq2 ⊢d=C→F⁡d=F⁡C
8 7 fveq1d ⊢d=C→F⁡d⁡i=F⁡C⁡i
9 8 breq2d ⊢d=C→0<F⁡d⁡i↔0<F⁡C⁡i
10 9 ralbidv ⊢d=C→∀i∈1…M+N0<F⁡d⁡i↔∀i∈1…M+N0<F⁡C⁡i
11 fveq2 ⊢c=d→F⁡c=F⁡d
12 11 fveq1d ⊢c=d→F⁡c⁡i=F⁡d⁡i
13 12 breq2d ⊢c=d→0<F⁡c⁡i↔0<F⁡d⁡i
14 13 ralbidv ⊢c=d→∀i∈1…M+N0<F⁡c⁡i↔∀i∈1…M+N0<F⁡d⁡i
15 14 cbvrabv ⊢c∈O|∀i∈1…M+N0<F⁡c⁡i=d∈O|∀i∈1…M+N0<F⁡d⁡i
16 6 15 eqtri ⊢E=d∈O|∀i∈1…M+N0<F⁡d⁡i
17 10 16 elrab2 ⊢C∈E↔C∈O∧∀i∈1…M+N0<F⁡C⁡i