Metamath Proof Explorer

Theorem ballotlem7

Description: R is a bijection between two subsets of ( O \ E ) : one where a vote for A is picked first, and one where a vote for B is picked first. (Contributed by Thierry Arnoux, 12-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
ballotth.mgtn ⊢ N < M
ballotth.i ⊢ I = c ∈ O ∖ E ⟼ inf k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
ballotth.r ⊢ R = c ∈ O ∖ E ⟼ S ⁡ c c
Assertion ballotlem7 ⊢ R ↾ c ∈ O ∖ E | 1 ∈ c : c ∈ O ∖ E | 1 ∈ c ⟶ 1-1 onto c ∈ O ∖ E | ¬ 1 ∈ c

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 ballotth.mgtn ⊢ N < M
8 ballotth.i ⊢ I = c ∈ O ∖ E ⟼ inf k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
9 ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
10 ballotth.r ⊢ R = c ∈ O ∖ E ⟼ S ⁡ c c
11 10 funmpt2 ⊢ Fun ⁡ R
12 1 2 3 4 5 6 7 8 9 10 ballotlemrinv ⊢ R -1 = R
13 rabid ⊢ c ∈ c ∈ O ∖ E | 1 ∈ c ↔ c ∈ O ∖ E ∧ 1 ∈ c
14 1 2 3 4 5 6 7 8 9 10 ballotlemrc ⊢ c ∈ O ∖ E → R ⁡ c ∈ O ∖ E
15 14 adantr ⊢ c ∈ O ∖ E ∧ 1 ∈ c → R ⁡ c ∈ O ∖ E
16 1 2 3 4 5 6 7 8 ballotlem1c ⊢ c ∈ O ∖ E ∧ 1 ∈ c → ¬ I ⁡ c ∈ c
17 16 ex ⊢ c ∈ O ∖ E → 1 ∈ c → ¬ I ⁡ c ∈ c
18 1 2 3 4 5 6 7 8 9 10 ballotlem1ri ⊢ c ∈ O ∖ E → 1 ∈ R ⁡ c ↔ I ⁡ c ∈ c
19 18 notbid ⊢ c ∈ O ∖ E → ¬ 1 ∈ R ⁡ c ↔ ¬ I ⁡ c ∈ c
20 17 19 sylibrd ⊢ c ∈ O ∖ E → 1 ∈ c → ¬ 1 ∈ R ⁡ c
21 20 imp ⊢ c ∈ O ∖ E ∧ 1 ∈ c → ¬ 1 ∈ R ⁡ c
22 15 21 jca ⊢ c ∈ O ∖ E ∧ 1 ∈ c → R ⁡ c ∈ O ∖ E ∧ ¬ 1 ∈ R ⁡ c
23 13 22 sylbi ⊢ c ∈ c ∈ O ∖ E | 1 ∈ c → R ⁡ c ∈ O ∖ E ∧ ¬ 1 ∈ R ⁡ c
24 23 rgen ⊢ ∀ c ∈ c ∈ O ∖ E | 1 ∈ c R ⁡ c ∈ O ∖ E ∧ ¬ 1 ∈ R ⁡ c
25 eleq2 ⊢ b = R ⁡ c → 1 ∈ b ↔ 1 ∈ R ⁡ c
26 25 notbid ⊢ b = R ⁡ c → ¬ 1 ∈ b ↔ ¬ 1 ∈ R ⁡ c
27 26 elrab ⊢ R ⁡ c ∈ b ∈ O ∖ E | ¬ 1 ∈ b ↔ R ⁡ c ∈ O ∖ E ∧ ¬ 1 ∈ R ⁡ c
28 eleq2 ⊢ b = c → 1 ∈ b ↔ 1 ∈ c
29 28 notbid ⊢ b = c → ¬ 1 ∈ b ↔ ¬ 1 ∈ c
30 29 cbvrabv ⊢ b ∈ O ∖ E | ¬ 1 ∈ b = c ∈ O ∖ E | ¬ 1 ∈ c
31 30 eleq2i ⊢ R ⁡ c ∈ b ∈ O ∖ E | ¬ 1 ∈ b ↔ R ⁡ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c
32 27 31 bitr3i ⊢ R ⁡ c ∈ O ∖ E ∧ ¬ 1 ∈ R ⁡ c ↔ R ⁡ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c
33 32 ralbii ⊢ ∀ c ∈ c ∈ O ∖ E | 1 ∈ c R ⁡ c ∈ O ∖ E ∧ ¬ 1 ∈ R ⁡ c ↔ ∀ c ∈ c ∈ O ∖ E | 1 ∈ c R ⁡ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c
34 24 33 mpbi ⊢ ∀ c ∈ c ∈ O ∖ E | 1 ∈ c R ⁡ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c
35 ssrab2 ⊢ c ∈ O ∖ E | 1 ∈ c ⊆ O ∖ E
36 fvex ⊢ S ⁡ c ∈ V
37 imaexg ⊢ S ⁡ c ∈ V → S ⁡ c c ∈ V
38 36 37 ax-mp ⊢ S ⁡ c c ∈ V
39 38 10 dmmpti ⊢ dom ⁡ R = O ∖ E
40 35 39 sseqtrri ⊢ c ∈ O ∖ E | 1 ∈ c ⊆ dom ⁡ R
41 nfrab1 ⊢ Ⅎ _ c c ∈ O ∖ E | 1 ∈ c
42 nfrab1 ⊢ Ⅎ _ c c ∈ O ∖ E | ¬ 1 ∈ c
43 nfmpt1 ⊢ Ⅎ _ c c ∈ O ∖ E ⟼ S ⁡ c c
44 10 43 nfcxfr ⊢ Ⅎ _ c R
45 41 42 44 funimass4f ⊢ Fun ⁡ R ∧ c ∈ O ∖ E | 1 ∈ c ⊆ dom ⁡ R → R c ∈ O ∖ E | 1 ∈ c ⊆ c ∈ O ∖ E | ¬ 1 ∈ c ↔ ∀ c ∈ c ∈ O ∖ E | 1 ∈ c R ⁡ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c
46 11 40 45 mp2an ⊢ R c ∈ O ∖ E | 1 ∈ c ⊆ c ∈ O ∖ E | ¬ 1 ∈ c ↔ ∀ c ∈ c ∈ O ∖ E | 1 ∈ c R ⁡ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c
47 34 46 mpbir ⊢ R c ∈ O ∖ E | 1 ∈ c ⊆ c ∈ O ∖ E | ¬ 1 ∈ c
48 rabid ⊢ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c ↔ c ∈ O ∖ E ∧ ¬ 1 ∈ c
49 14 adantr ⊢ c ∈ O ∖ E ∧ ¬ 1 ∈ c → R ⁡ c ∈ O ∖ E
50 1 2 3 4 5 6 7 8 ballotlemic ⊢ c ∈ O ∖ E ∧ ¬ 1 ∈ c → I ⁡ c ∈ c
51 50 ex ⊢ c ∈ O ∖ E → ¬ 1 ∈ c → I ⁡ c ∈ c
52 51 18 sylibrd ⊢ c ∈ O ∖ E → ¬ 1 ∈ c → 1 ∈ R ⁡ c
53 52 imp ⊢ c ∈ O ∖ E ∧ ¬ 1 ∈ c → 1 ∈ R ⁡ c
54 49 53 jca ⊢ c ∈ O ∖ E ∧ ¬ 1 ∈ c → R ⁡ c ∈ O ∖ E ∧ 1 ∈ R ⁡ c
55 48 54 sylbi ⊢ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c → R ⁡ c ∈ O ∖ E ∧ 1 ∈ R ⁡ c
56 55 rgen ⊢ ∀ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c R ⁡ c ∈ O ∖ E ∧ 1 ∈ R ⁡ c
57 25 elrab ⊢ R ⁡ c ∈ b ∈ O ∖ E | 1 ∈ b ↔ R ⁡ c ∈ O ∖ E ∧ 1 ∈ R ⁡ c
58 28 cbvrabv ⊢ b ∈ O ∖ E | 1 ∈ b = c ∈ O ∖ E | 1 ∈ c
59 58 eleq2i ⊢ R ⁡ c ∈ b ∈ O ∖ E | 1 ∈ b ↔ R ⁡ c ∈ c ∈ O ∖ E | 1 ∈ c
60 57 59 bitr3i ⊢ R ⁡ c ∈ O ∖ E ∧ 1 ∈ R ⁡ c ↔ R ⁡ c ∈ c ∈ O ∖ E | 1 ∈ c
61 60 ralbii ⊢ ∀ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c R ⁡ c ∈ O ∖ E ∧ 1 ∈ R ⁡ c ↔ ∀ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c R ⁡ c ∈ c ∈ O ∖ E | 1 ∈ c
62 56 61 mpbi ⊢ ∀ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c R ⁡ c ∈ c ∈ O ∖ E | 1 ∈ c
63 ssrab2 ⊢ c ∈ O ∖ E | ¬ 1 ∈ c ⊆ O ∖ E
64 63 39 sseqtrri ⊢ c ∈ O ∖ E | ¬ 1 ∈ c ⊆ dom ⁡ R
65 42 41 44 funimass4f ⊢ Fun ⁡ R ∧ c ∈ O ∖ E | ¬ 1 ∈ c ⊆ dom ⁡ R → R c ∈ O ∖ E | ¬ 1 ∈ c ⊆ c ∈ O ∖ E | 1 ∈ c ↔ ∀ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c R ⁡ c ∈ c ∈ O ∖ E | 1 ∈ c
66 11 64 65 mp2an ⊢ R c ∈ O ∖ E | ¬ 1 ∈ c ⊆ c ∈ O ∖ E | 1 ∈ c ↔ ∀ c ∈ c ∈ O ∖ E | ¬ 1 ∈ c R ⁡ c ∈ c ∈ O ∖ E | 1 ∈ c
67 62 66 mpbir ⊢ R c ∈ O ∖ E | ¬ 1 ∈ c ⊆ c ∈ O ∖ E | 1 ∈ c
68 11 12 47 67 40 64 rinvf1o ⊢ R ↾ c ∈ O ∖ E | 1 ∈ c : c ∈ O ∖ E | 1 ∈ c ⟶ 1-1 onto c ∈ O ∖ E | ¬ 1 ∈ c