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 ⟼ x O
ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
Assertion ballotleme ⊢ C ∈ E ↔ C ∈ O ∧ ∀ i ∈ 1 … M + N 0 < 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 ⟼ x O
5 ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
6 ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < 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 + N 0 < F ⁡ d ⁡ i ↔ ∀ i ∈ 1 … M + N 0 < 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 + N 0 < F ⁡ c ⁡ i ↔ ∀ i ∈ 1 … M + N 0 < F ⁡ d ⁡ i
15 14 cbvrabv ⊢ c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i = d ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ d ⁡ i
16 6 15 eqtri ⊢ E = d ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ d ⁡ i
17 10 16 elrab2 ⊢ C ∈ E ↔ C ∈ O ∧ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i